--- a/doc-src/ZF/FOL_examples.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-header{*Examples of Classical Reasoning*}
-
-theory FOL_examples imports "~~/src/FOL/FOL" begin
-
-lemma "EX y. ALL x. P(y)-->P(x)"
- --{* @{subgoals[display,indent=0,margin=65]} *}
-apply (rule exCI)
- --{* @{subgoals[display,indent=0,margin=65]} *}
-apply (rule allI)
- --{* @{subgoals[display,indent=0,margin=65]} *}
-apply (rule impI)
- --{* @{subgoals[display,indent=0,margin=65]} *}
-apply (erule allE)
- --{* @{subgoals[display,indent=0,margin=65]} *}
-txt{*see below for @{text allI} combined with @{text swap}*}
-apply (erule allI [THEN [2] swap])
- --{* @{subgoals[display,indent=0,margin=65]} *}
-apply (rule impI)
- --{* @{subgoals[display,indent=0,margin=65]} *}
-apply (erule notE)
- --{* @{subgoals[display,indent=0,margin=65]} *}
-apply assumption
-done
-
-text {*
-@{thm[display] allI [THEN [2] swap]}
-*}
-
-lemma "EX y. ALL x. P(y)-->P(x)"
-by blast
-
-end
-
-