src/HOL/HOL.thy

   The following copy of the implication operator is useful for
   fine-tuning congruence rules.  It instructs the simplifier to simplify
   its premise.
 *}
 
-constdefs
-  simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1)
+definition simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1) where
   [code del]: "simp_implies \<equiv> op ==>"
 
 lemma simp_impliesI:
   assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
   shows "PROP P =simp=> PROP Q"

   val conjunct2 = @{thm conjunct2}
   val mp = @{thm mp}
 )
 *}
 
-constdefs
-  induct_forall where "induct_forall P == \<forall>x. P x"
-  induct_implies where "induct_implies A B == A \<longrightarrow> B"
-  induct_equal where "induct_equal x y == x = y"
-  induct_conj where "induct_conj A B == A \<and> B"
-  induct_true where "induct_true == True"
-  induct_false where "induct_false == False"
+definition induct_forall where
+  "induct_forall P == \<forall>x. P x"
+
+definition induct_implies where
+  "induct_implies A B == A \<longrightarrow> B"
+
+definition induct_equal where
+  "induct_equal x y == x = y"
+
+definition induct_conj where
+  "induct_conj A B == A \<and> B"
+
+definition induct_true where
+  "induct_true == True"
+
+definition induct_false where
+  "induct_false == False"
 
 lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))"
   by (unfold atomize_all induct_forall_def)
 
 lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)"