--- a/src/FOL/FOL.thy Thu Apr 09 15:54:09 2015 +0200
+++ b/src/FOL/FOL.thy Thu Apr 09 20:42:32 2015 +0200
@@ -387,10 +387,10 @@
context
begin
-restricted definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
-restricted definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
-restricted definition "induct_equal(x, y) \<equiv> x = y"
-restricted definition "induct_conj(A, B) \<equiv> A \<and> B"
+qualified definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
+qualified definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
+qualified definition "induct_equal(x, y) \<equiv> x = y"
+qualified definition "induct_conj(A, B) \<equiv> A \<and> B"
lemma induct_forall_eq: "(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))"
unfolding atomize_all induct_forall_def .