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.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
```