On 25.08.2015 18:16, Lars Noschinski wrote: > Hi everyone, > Unfortunately, simps_of_case cannot use the Splitter, as splitter > applies the split-rule in the wrong direction. So simps_of_case either > needs to reimplement the Splitter's logic for instantiating the split > rule or the Splitter needs to be refactored generate the instantiated > equation.
That being said, a shortcut is possible if one requires the equation given to simps_of_case to be of the form "... = case x of ..." Does anyone rely on the more liberal form "... = P (case x of ...)" accepted at the moment? _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
