Hi, Attempting to define
fun f where "f 0 = undefined" in Isabelle/HOL (7f2793d51efc) yields *** exception TYPE raised (line 38 of ".../isabelle/src/HOL/Tools/Function/pattern_split.ML"): inst_constrs_of *** At command "fun" A more user-friendly error message would be nice. Kind regards, Tjark _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
