src/HOL/HOL.thy
changeset 59940 087d81f5213e
parent 59929 a090551e5ec8
child 59970 e9f73d87d904
     1.1 --- a/src/HOL/HOL.thy	Mon Apr 06 22:11:01 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Apr 06 23:14:05 2015 +0200
     1.3 @@ -1374,12 +1374,15 @@
     1.4  );
     1.5  *}
     1.6  
     1.7 -definition "induct_forall P \<equiv> \<forall>x. P x"
     1.8 -definition "induct_implies A B \<equiv> A \<longrightarrow> B"
     1.9 -definition "induct_equal x y \<equiv> x = y"
    1.10 -definition "induct_conj A B \<equiv> A \<and> B"
    1.11 -definition "induct_true \<equiv> True"
    1.12 -definition "induct_false \<equiv> False"
    1.13 +context
    1.14 +begin
    1.15 +
    1.16 +restricted definition "induct_forall P \<equiv> \<forall>x. P x"
    1.17 +restricted definition "induct_implies A B \<equiv> A \<longrightarrow> B"
    1.18 +restricted definition "induct_equal x y \<equiv> x = y"
    1.19 +restricted definition "induct_conj A B \<equiv> A \<and> B"
    1.20 +restricted definition "induct_true \<equiv> True"
    1.21 +restricted definition "induct_false \<equiv> False"
    1.22  
    1.23  lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
    1.24    by (unfold atomize_all induct_forall_def)
    1.25 @@ -1444,8 +1447,8 @@
    1.26  
    1.27  ML_file "~~/src/Tools/induction.ML"
    1.28  
    1.29 -setup {*
    1.30 -  Context.theory_map (Induct.map_simpset (fn ss => ss
    1.31 +declaration {*
    1.32 +  fn _ => Induct.map_simpset (fn ss => ss
    1.33      addsimprocs
    1.34        [Simplifier.simproc_global @{theory} "swap_induct_false"
    1.35           ["induct_false ==> PROP P ==> PROP Q"]
    1.36 @@ -1468,7 +1471,7 @@
    1.37                | _ => NONE))]
    1.38      |> Simplifier.set_mksimps (fn ctxt =>
    1.39          Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
    1.40 -        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
    1.41 +        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
    1.42  *}
    1.43  
    1.44  text {* Pre-simplification of induction and cases rules *}
    1.45 @@ -1523,7 +1526,7 @@
    1.46  lemma [induct_simp]: "x = x \<longleftrightarrow> True"
    1.47    by (rule simp_thms)
    1.48  
    1.49 -hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
    1.50 +end
    1.51  
    1.52  ML_file "~~/src/Tools/induct_tacs.ML"
    1.53