src/HOL/Partial_Function.thy

 by(auto simp add: flat_ord_def)
 
 lemma antisymP_flat_ord: "antisymP (flat_ord a)"
 by(rule antisymI)(auto dest: flat_ord_antisym)
 
-interpretation tailrec!:
+interpretation tailrec:
   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
   rewrites "flat_lub undefined {} \<equiv> undefined"
 by (rule flat_interpretation)(simp add: flat_lub_def)
 
-interpretation option!:
+interpretation option:
   partial_function_definitions "flat_ord None" "flat_lub None"
   rewrites "flat_lub None {} \<equiv> None"
 by (rule flat_interpretation)(simp add: flat_lub_def)