src/HOL/FunDef.thy

 
 
 section {* Definitions with default value *}
 
 definition
-  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
+  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
   "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)"
 
 lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
   by (simp add:theI' THE_default_def)
 

 intros
   "(Inl x, x) : lpg"
 inductive rpg
 intros
   "(Inr y, y) : rpg"
-definition
-  "lproj x = (THE y. (x,y) : lpg)"
-  "rproj x = (THE y. (x,y) : rpg)"
+
+definition "lproj x = (THE y. (x,y) : lpg)"
+definition "rproj x = (THE y. (x,y) : rpg)"
 
 lemma lproj_inl:
   "lproj (Inl x) = x"
   by (auto simp:lproj_def intro: the_equality lpg.intros elim: lpg.cases)
 lemma rproj_inr: