src/FOL/FOL.thy
changeset 59940 087d81f5213e
parent 59780 23b67731f4f0
child 59942 6a3098313acf
     1.1 --- a/src/FOL/FOL.thy	Mon Apr 06 22:11:01 2015 +0200
     1.2 +++ b/src/FOL/FOL.thy	Mon Apr 06 23:14:05 2015 +0200
     1.3 @@ -384,10 +384,13 @@
     1.4  
     1.5  text {* Proper handling of non-atomic rule statements. *}
     1.6  
     1.7 -definition "induct_forall(P) == \<forall>x. P(x)"
     1.8 -definition "induct_implies(A, B) == A \<longrightarrow> B"
     1.9 -definition "induct_equal(x, y) == x = y"
    1.10 -definition "induct_conj(A, B) == A \<and> B"
    1.11 +context
    1.12 +begin
    1.13 +
    1.14 +restricted definition "induct_forall(P) == \<forall>x. P(x)"
    1.15 +restricted definition "induct_implies(A, B) == A \<longrightarrow> B"
    1.16 +restricted definition "induct_equal(x, y) == x = y"
    1.17 +restricted definition "induct_conj(A, B) == A \<and> B"
    1.18  
    1.19  lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
    1.20    unfolding atomize_all induct_forall_def .
    1.21 @@ -406,9 +409,6 @@
    1.22  lemmas induct_rulify_fallback =
    1.23    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.24  
    1.25 -hide_const induct_forall induct_implies induct_equal induct_conj
    1.26 -
    1.27 -
    1.28  text {* Method setup. *}
    1.29  
    1.30  ML_file "~~/src/Tools/induct.ML"
    1.31 @@ -427,6 +427,8 @@
    1.32  
    1.33  declare case_split [cases type: o]
    1.34  
    1.35 +end
    1.36 +
    1.37  ML_file "~~/src/Tools/case_product.ML"
    1.38  
    1.39