# HG changeset patch
# User wenzelm
# Date 1138465730 -3600
# Node ID aebd7f315b924409b65dbfa12f01c7caa03f0d0e
# Parent  cb778c0ce1b5b6ae15ba96f82c31521f1a0b6e34
tuned proofs;

diff -r cb778c0ce1b5 -r aebd7f315b92 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sat Jan 28 17:28:48 2006 +0100
+++ b/src/FOL/FOL.thy	Sat Jan 28 17:28:50 2006 +0100
@@ -90,18 +90,18 @@
   induct_conj where "induct_conj(A, B) == A \<and> B"
 
 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
-  by (unfold atomize_all induct_forall_def)
+  unfolding atomize_all induct_forall_def .
 
 lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))"
-  by (unfold atomize_imp induct_implies_def)
+  unfolding atomize_imp induct_implies_def .
 
 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
-  by (unfold atomize_eq induct_equal_def)
+  unfolding atomize_eq induct_equal_def .
 
 lemma induct_conj_eq:
   includes meta_conjunction_syntax
   shows "(A && B) == Trueprop(induct_conj(A, B))"
-  by (unfold atomize_conj induct_conj_def)
+  unfolding atomize_conj induct_conj_def .
 
 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
 lemmas induct_rulify [symmetric, standard] = induct_atomize