* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax for pattern aliases as known from Haskell, Scala and ML.
This is a small library theory providing convenient syntax for defining recursive functions. Tobias is already using this for defining functions over trees. For example: function merge :: "('a::linorder) heap ⇒ 'a heap ⇒ 'a heap" where "merge Leaf h = h" | "merge h Leaf = h" | "merge (Node l1 a1 r1 =: h1) (Node l2 a2 r2 =: h2) = (if a1 ≤ a2 then Node (merge h2 r1) a1 l1 else Node (merge h1 r2) a2 l2)" Users of Haskell or Scala should be familiar with this syntax (both use "@" instead of "=:", but "@" is already used in HOL). To use this syntax, you need to import "HOL-Library.Pattern_Aliases" and activate the bundle "pattern_aliases" either locally or globally. I recommend doing this only locally, i.e. context includes pattern_aliases begin (* ... *) end This avoids polluting the global syntax. Some more documentation can be found in the theory file. There is still time to tweak this for the 2017 release, so comments are welcome. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev