src/HOL/HOL.thy
changeset 59990 a81dc82ecba3
parent 59970 e9f73d87d904
child 60143 2cd31c81e0e7
     1.1 --- a/src/HOL/HOL.thy	Thu Apr 09 15:54:09 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Apr 09 20:42:32 2015 +0200
     1.3 @@ -1377,12 +1377,12 @@
     1.4  context
     1.5  begin
     1.6  
     1.7 -restricted definition "induct_forall P \<equiv> \<forall>x. P x"
     1.8 -restricted definition "induct_implies A B \<equiv> A \<longrightarrow> B"
     1.9 -restricted definition "induct_equal x y \<equiv> x = y"
    1.10 -restricted definition "induct_conj A B \<equiv> A \<and> B"
    1.11 -restricted definition "induct_true \<equiv> True"
    1.12 -restricted definition "induct_false \<equiv> False"
    1.13 +qualified definition "induct_forall P \<equiv> \<forall>x. P x"
    1.14 +qualified definition "induct_implies A B \<equiv> A \<longrightarrow> B"
    1.15 +qualified definition "induct_equal x y \<equiv> x = y"
    1.16 +qualified definition "induct_conj A B \<equiv> A \<and> B"
    1.17 +qualified definition "induct_true \<equiv> True"
    1.18 +qualified definition "induct_false \<equiv> False"
    1.19  
    1.20  lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
    1.21    by (unfold atomize_all induct_forall_def)