src/FOL/FOL.thy

 
 subsection {* Proof by cases and induction *}
 
 text {* Proper handling of non-atomic rule statements. *}
 
-definition "induct_forall(P) == \<forall>x. P(x)"
-definition "induct_implies(A, B) == A \<longrightarrow> B"
-definition "induct_equal(x, y) == x = y"
-definition "induct_conj(A, B) == A \<and> B"
+context
+begin
+
+restricted definition "induct_forall(P) == \<forall>x. P(x)"
+restricted definition "induct_implies(A, B) == A \<longrightarrow> B"
+restricted definition "induct_equal(x, y) == x = y"
+restricted definition "induct_conj(A, B) == A \<and> B"
 
 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
   unfolding atomize_all induct_forall_def .
 
 lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))"

 
 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
 lemmas induct_rulify [symmetric] = induct_atomize
 lemmas induct_rulify_fallback =
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
-
-hide_const induct_forall induct_implies induct_equal induct_conj
-
 
 text {* Method setup. *}
 
 ML_file "~~/src/Tools/induct.ML"
 ML {*

   );
 *}
 
 declare case_split [cases type: o]
 
+end
+
 ML_file "~~/src/Tools/case_product.ML"
 
 
 hide_const (open) eq