Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/FOL/FOL.thy
changeset 28699 32b6a8f12c1c
parent 27882 eaa9fef9f4c1
child 28856 5e009a80fe6d 
--- a/src/FOL/FOL.thy	Mon Oct 27 18:14:34 2008 +0100
+++ b/src/FOL/FOL.thy	Tue Oct 28 11:03:07 2008 +0100
@@ -347,7 +347,7 @@
   unfolding atomize_eq induct_equal_def .
 
 lemma induct_conj_eq:
-  includes meta_conjunction_syntax
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   shows "(A && B) == Trueprop(induct_conj(A, B))"
   unfolding atomize_conj induct_conj_def .
isabelle