removed obsolete ML files;

--- a/src/FOL/IsaMakefile	Wed Jun 07 16:55:39 2006 +0200
+++ b/src/FOL/IsaMakefile	Wed Jun 07 23:21:55 2006 +0200
@@ -45,9 +45,9 @@
 
 $(LOG)/FOL-ex.gz: $(OUT)/FOL$(ML_SUFFIX) ex/First_Order_Logic.thy \
   ex/If.thy ex/IffOracle.thy ex/List.ML ex/List.thy ex/LocaleTest.thy \
-  ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy	\
-  ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
-  ex/foundn.ML ex/Intuitionistic.thy ex/intro.ML ex/prop.ML ex/quant.ML
+  ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy	\
+  ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
+  ex/Foundation.thy ex/Intuitionistic.thy ex/Intro.thy ex/prop.ML ex/quant.ML
 	@$(ISATOOL) usedir $(OUT)/FOL ex
 
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/Foundation.thy	Wed Jun 07 23:21:55 2006 +0200
@@ -0,0 +1,135 @@
+(*  Title:      FOL/ex/Foundation.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+*)
+
+header "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"
+
+theory Foundation
+imports IFOL
+begin
+
+lemma "A&B  --> (C-->A&C)"
+apply (rule impI)
+apply (rule impI)
+apply (rule conjI)
+prefer 2 apply assumption
+apply (rule conjunct1)
+apply assumption
+done
+
+text {*A form of conj-elimination*}
+lemma
+  assumes "A & B"
+    and "A ==> B ==> C"
+  shows C
+apply (rule prems)
+apply (rule conjunct1)
+apply (rule prems)
+apply (rule conjunct2)
+apply (rule prems)
+done
+
+lemma
+  assumes "!!A. ~ ~A ==> A"
+  shows "B | ~B"
+apply (rule prems)
+apply (rule notI)
+apply (rule_tac P = "~B" in notE)
+apply (rule_tac [2] notI)
+apply (rule_tac [2] P = "B | ~B" in notE)
+prefer 2 apply assumption
+apply (rule_tac [2] disjI1)
+prefer 2 apply assumption
+apply (rule notI)
+apply (rule_tac P = "B | ~B" in notE)
+apply assumption
+apply (rule disjI2)
+apply assumption
+done
+
+lemma
+  assumes "!!A. ~ ~A ==> A"
+  shows "B | ~B"
+apply (rule prems)
+apply (rule notI)
+apply (rule notE)
+apply (rule_tac [2] notI)
+apply (erule_tac [2] notE)
+apply (erule_tac [2] disjI1)
+apply (rule notI)
+apply (erule notE)
+apply (erule disjI2)
+done
+
+
+lemma
+  assumes "A | ~A"
+    and "~ ~A"
+  shows A
+apply (rule disjE)
+apply (rule prems)
+apply assumption
+apply (rule FalseE)
+apply (rule_tac P = "~A" in notE)
+apply (rule prems)
+apply assumption
+done
+
+
+subsection "Examples with quantifiers"
+
+lemma
+  assumes "ALL z. G(z)"
+  shows "ALL z. G(z)|H(z)"
+apply (rule allI)
+apply (rule disjI1)
+apply (rule prems [THEN spec])
+done
+
+lemma "ALL x. EX y. x=y"
+apply (rule allI)
+apply (rule exI)
+apply (rule refl)
+done
+
+lemma "EX y. ALL x. x=y"
+apply (rule exI)
+apply (rule allI)
+apply (rule refl)?
+oops
+
+text {* Parallel lifting example. *}
+lemma "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
+apply (rule exI allI)
+apply (rule exI allI)
+apply (rule exI allI)
+apply (rule exI allI)
+apply (rule exI allI)
+oops
+
+lemma
+  assumes "(EX z. F(z)) & B"
+  shows "EX z. F(z) & B"
+apply (rule conjE)
+apply (rule prems)
+apply (rule exE)
+apply assumption
+apply (rule exI)
+apply (rule conjI)
+apply assumption
+apply assumption
+done
+
+text {* A bigger demonstration of quantifiers -- not in the paper. *}
+lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
+apply (rule impI)
+apply (rule allI)
+apply (rule exE, assumption)
+apply (rule exI)
+apply (rule allE, assumption)
+apply assumption
+done
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/Intro.thy	Wed Jun 07 23:21:55 2006 +0200
@@ -0,0 +1,102 @@
+(*  Title:      FOL/ex/Intro.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Derives some inference rules, illustrating the use of definitions.
+*)
+
+header {* Examples for the manual ``Introduction to Isabelle'' *}
+
+theory Intro
+imports FOL
+begin
+
+subsubsection {* Some simple backward proofs *}
+
+lemma mythm: "P|P --> P"
+apply (rule impI)
+apply (rule disjE)
+prefer 3 apply (assumption)
+prefer 2 apply (assumption)
+apply assumption
+done
+
+lemma "(P & Q) | R --> (P | R)"
+apply (rule impI)
+apply (erule disjE)
+apply (drule conjunct1)
+apply (rule disjI1)
+apply (rule_tac [2] disjI2)
+apply assumption+
+done
+
+(*Correct version, delaying use of "spec" until last*)
+lemma "(ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
+apply (rule impI)
+apply (rule allI)
+apply (rule allI)
+apply (drule spec)
+apply (drule spec)
+apply assumption
+done
+
+
+subsubsection {* Demonstration of @{text "fast"} *}
+
+lemma "(EX y. ALL x. J(y,x) <-> ~J(x,x))
+        -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
+apply fast
+done
+
+
+lemma "ALL x. P(x,f(x)) <->
+        (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
+apply fast
+done
+
+
+subsubsection {* Derivation of conjunction elimination rule *}
+
+lemma
+  assumes major: "P&Q"
+    and minor: "[| P; Q |] ==> R"
+  shows R
+apply (rule minor)
+apply (rule major [THEN conjunct1])
+apply (rule major [THEN conjunct2])
+done
+
+
+subsection {* Derived rules involving definitions *}
+
+text {* Derivation of negation introduction *}
+
+lemma
+  assumes "P ==> False"
+  shows "~ P"
+apply (unfold not_def)
+apply (rule impI)
+apply (rule prems)
+apply assumption
+done
+
+lemma
+  assumes major: "~P"
+    and minor: P
+  shows R
+apply (rule FalseE)
+apply (rule mp)
+apply (rule major [unfolded not_def])
+apply (rule minor)
+done
+
+text {* Alternative proof of the result above *}
+lemma
+  assumes major: "~P"
+    and minor: P
+  shows R
+apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])
+done
+
+end

--- a/src/FOL/ex/Nat.ML	Wed Jun 07 16:55:39 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  Title:      FOL/ex/Nat.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Proofs about the natural numbers.
-
-To generate similar output to manual, execute these commands:
-    Pretty.setmargin 72; print_depth 0;
-*)
-
-Goal "Suc(k) ~= k";
-by (res_inst_tac [("n","k")] induct 1);
-by (rtac notI 1);
-by (etac Suc_neq_0 1);
-by (rtac notI 1);
-by (etac notE 1);
-by (etac Suc_inject 1);
-qed "Suc_n_not_n";
-
-
-Goal "(k+m)+n = k+(m+n)";
-prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
-by (rtac induct 1);
-back();
-back();
-back();
-back();
-back();
-back();
-
-Goalw [add_def] "0+n = n";
-by (rtac rec_0 1);
-qed "add_0";
-
-Goalw [add_def] "Suc(m)+n = Suc(m+n)";
-by (rtac rec_Suc 1);
-qed "add_Suc";
-
-Addsimps [add_0, add_Suc];
-
-Goal "(k+m)+n = k+(m+n)";
-by (res_inst_tac [("n","k")] induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_assoc";
-
-Goal "m+0 = m";
-by (res_inst_tac [("n","m")] induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_0_right";
-
-Goal "m+Suc(n) = Suc(m+n)";
-by (res_inst_tac [("n","m")] induct 1);
-by (ALLGOALS (Asm_simp_tac));
-qed "add_Suc_right";
-
-(*Example used in Reference Manual, Doc/Ref/simplifier.tex*)
-val [prem] = Goal "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
-by (res_inst_tac [("n","i")] induct 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [prem]) 1);
-result();

--- a/src/FOL/ex/Nat.thy	Wed Jun 07 16:55:39 2006 +0200
+++ b/src/FOL/ex/Nat.thy	Wed Jun 07 23:21:55 2006 +0200
@@ -25,8 +25,65 @@
   Suc_neq_0:   "Suc(m)=0      ==> R"
   rec_0:       "rec(0,a,f) = a"
   rec_Suc:     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
+
+defs
   add_def:     "m+n == rec(m, n, %x y. Suc(y))"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+subsection {* Proofs about the natural numbers *}
+
+lemma Suc_n_not_n: "Suc(k) ~= k"
+apply (rule_tac n = k in induct)
+apply (rule notI)
+apply (erule Suc_neq_0)
+apply (rule notI)
+apply (erule notE)
+apply (erule Suc_inject)
+done
+
+lemma "(k+m)+n = k+(m+n)"
+apply (rule induct)
+back
+back
+back
+back
+back
+back
+oops
+
+lemma add_0 [simp]: "0+n = n"
+apply (unfold add_def)
+apply (rule rec_0)
+done
+
+lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)"
+apply (unfold add_def)
+apply (rule rec_Suc)
+done
+
+lemma add_assoc: "(k+m)+n = k+(m+n)"
+apply (rule_tac n = k in induct)
+apply simp
+apply simp
+done
+
+lemma add_0_right: "m+0 = m"
+apply (rule_tac n = m in induct)
+apply simp
+apply simp
+done
+
+lemma add_Suc_right: "m+Suc(n) = Suc(m+n)"
+apply (rule_tac n = m in induct)
+apply simp_all
+done
+
+lemma
+  assumes prem: "!!n. f(Suc(n)) = Suc(f(n))"
+  shows "f(i+j) = i+f(j)"
+apply (rule_tac n = i in induct)
+apply simp
+apply (simp add: prem)
+done
 
 end

--- a/src/FOL/ex/NatClass.ML	Wed Jun 07 16:55:39 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(*  Title:      FOL/ex/NatClass.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-This is Nat.ML trivially modified to make it work with NatClass.thy.
-*)
-
-Goal "Suc(k) ~= (k::'a::nat)";
-by (res_inst_tac [("n","k")] induct 1);
-by (rtac notI 1);
-by (etac Suc_neq_0 1);
-by (rtac notI 1);
-by (etac notE 1);
-by (etac Suc_inject 1);
-qed "Suc_n_not_n";
-
-
-Goal "(k+m)+n = k+(m+n)";
-prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
-by (rtac induct 1);
-back();
-back();
-back();
-back();
-back();
-back();
-
-Goalw [add_def] "0+n = n";
-by (rtac rec_0 1);
-qed "add_0";
-
-Goalw [add_def] "Suc(m)+n = Suc(m+n)";
-by (rtac rec_Suc 1);
-qed "add_Suc";
-
-Addsimps [add_0, add_Suc];
-
-Goal "(k+m)+n = k+(m+n)";
-by (res_inst_tac [("n","k")] induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_assoc";
-
-Goal "m+0 = m";
-by (res_inst_tac [("n","m")] induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_0_right";
-
-Goal "m+Suc(n) = Suc(m+n)";
-by (res_inst_tac [("n","m")] induct 1);
-by (ALLGOALS (Asm_simp_tac));
-qed "add_Suc_right";
-
-val [prem] = goal (the_context ()) "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
-by (res_inst_tac [("n","i")] induct 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [prem]) 1);
-result();

--- a/src/FOL/ex/NatClass.thy	Wed Jun 07 16:55:39 2006 +0200
+++ b/src/FOL/ex/NatClass.thy	Wed Jun 07 23:21:55 2006 +0200
@@ -29,11 +29,62 @@
   rec_0:         "rec(0, a, f) = a"
   rec_Suc:       "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
 
-constdefs
+definition
   add :: "['a::nat, 'a] => 'a"    (infixl "+" 60)
-  "m + n == rec(m, n, %x y. Suc(y))"
+  "m + n = rec(m, n, %x y. Suc(y))"
+
+lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)"
+apply (rule_tac n = k in induct)
+apply (rule notI)
+apply (erule Suc_neq_0)
+apply (rule notI)
+apply (erule notE)
+apply (erule Suc_inject)
+done
+
+lemma "(k+m)+n = k+(m+n)"
+apply (rule induct)
+back
+back
+back
+back
+back
+back
+oops
+
+lemma add_0 [simp]: "0+n = n"
+apply (unfold add_def)
+apply (rule rec_0)
+done
 
-ML {* use_legacy_bindings (the_context ()) *}
-ML {* open nat_class *}
+lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)"
+apply (unfold add_def)
+apply (rule rec_Suc)
+done
+
+lemma add_assoc: "(k+m)+n = k+(m+n)"
+apply (rule_tac n = k in induct)
+apply simp
+apply simp
+done
+
+lemma add_0_right: "m+0 = m"
+apply (rule_tac n = m in induct)
+apply simp
+apply simp
+done
+
+lemma add_Suc_right: "m+Suc(n) = Suc(m+n)"
+apply (rule_tac n = m in induct)
+apply simp_all
+done
+
+lemma
+  assumes prem: "!!n. f(Suc(n)) = Suc(f(n))"
+  shows "f(i+j) = i+f(j)"
+apply (rule_tac n = i in induct)
+apply simp
+apply (simp add: prem)
+done
 
 end

--- a/src/FOL/ex/Prolog.ML	Wed Jun 07 16:55:39 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(*  Title:      FOL/ex/prolog.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-*)
-
-Goal "app(a:b:c:Nil, d:e:Nil, ?x)";
-by (resolve_tac [appNil,appCons] 1);
-by (resolve_tac [appNil,appCons] 1);
-by (resolve_tac [appNil,appCons] 1);
-by (resolve_tac [appNil,appCons] 1);
-prth (result());
-
-Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
-by (REPEAT (resolve_tac [appNil,appCons] 1));
-result();
-
-
-Goal "app(?x, ?y, a:b:c:d:Nil)";
-by (REPEAT (resolve_tac [appNil,appCons] 1));
-back();
-back();
-back();
-back();
-result();
-
-
-(*app([x1,...,xn], y, ?z) requires (n+1) inferences*)
-(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*)
-
-Goal "rev(a:b:c:d:Nil, ?x)";
-val rules = [appNil,appCons,revNil,revCons];
-by (REPEAT (resolve_tac rules 1));
-result();
-
-Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
-by (REPEAT (resolve_tac rules 1));
-result();
-
-Goal "rev(?x, a:b:c:Nil)";
-by (REPEAT (resolve_tac rules 1)); (*does not solve it directly!*)
-back();
-back();
-
-(*backtracking version*)
-val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1);
-
-choplev 0;
-by prolog_tac;
-result();
-
-Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
-by prolog_tac;
-result();
-
-(*rev([a..p], ?w) requires 153 inferences *)
-Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)";
-by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
-(*Poly/ML: 4 secs >> 38 lips*)
-result();
-
-(*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences;
-  total inferences = 2 + 1 + 17 + 561 = 581*)
-Goal
-    "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)";
-by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
-(*Poly/ML: 29 secs >> 20 lips*)
-result();

--- a/src/FOL/ex/Prolog.thy	Wed Jun 07 16:55:39 2006 +0200
+++ b/src/FOL/ex/Prolog.thy	Wed Jun 07 23:21:55 2006 +0200
@@ -23,6 +23,66 @@
   revNil:  "rev(Nil,Nil)"
   revCons: "[| rev(xs,ys);  app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
+apply (rule appNil appCons)
+apply (rule appNil appCons)
+apply (rule appNil appCons)
+apply (rule appNil appCons)
+done
+
+lemma "app(?x, c:d:Nil, a:b:c:d:Nil)"
+apply (rule appNil appCons)+
+done
+
+lemma "app(?x, ?y, a:b:c:d:Nil)"
+apply (rule appNil appCons)+
+back
+back
+back
+back
+done
+
+(*app([x1,...,xn], y, ?z) requires (n+1) inferences*)
+(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*)
+
+lemmas rules = appNil appCons revNil revCons
+
+lemma "rev(a:b:c:d:Nil, ?x)"
+apply (rule rules)+
+done
+
+lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"
+apply (rule rules)+
+done
+
+lemma "rev(?x, a:b:c:Nil)"
+apply (rule rules)+  -- {* does not solve it directly! *}
+back
+back
+done
+
+(*backtracking version*)
+ML {*
+val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (thms "rules") 1)
+*}
+
+lemma "rev(?x, a:b:c:Nil)"
+apply (tactic prolog_tac)
+done
+
+lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)"
+apply (tactic prolog_tac)
+done
+
+(*rev([a..p], ?w) requires 153 inferences *)
+lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
+apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})
+done
+
+(*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences
+  total inferences = 2 + 1 + 17 + 561 = 581*)
+lemma "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"
+apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})
+done
 
 end

--- a/src/FOL/ex/ROOT.ML	Wed Jun 07 16:55:39 2006 +0200
+++ b/src/FOL/ex/ROOT.ML	Wed Jun 07 23:21:55 2006 +0200
@@ -8,12 +8,11 @@
 
 time_use_thy "First_Order_Logic";
 time_use_thy "Natural_Numbers";
-time_use     "intro.ML";
+time_use_thy "Intro";
 time_use_thy "Nat";
-time_use     "foundn.ML";
+time_use_thy "Foundation";
 time_use_thy "Prolog";
 
-writeln"\n** Intuitionistic examples **\n";
 time_use_thy "Intuitionistic";
 
 val thy = IFOL.thy  and  tac = IntPr.fast_tac 1;
@@ -35,7 +34,6 @@
 time_use_thy "Nat2";
 time_use_thy "List";
 
-writeln"\n** How to declare an oracle **\n";
 time_use_thy "IffOracle";
 
 (*regression test for locales -- sets several global flags!*)

--- a/src/FOL/ex/foundn.ML	Wed Jun 07 16:55:39 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-(*  Title:      FOL/ex/foundn.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
-*)
-
-goal IFOL.thy "A&B  --> (C-->A&C)";
-by (rtac impI 1);
-by (rtac impI 1);
-by (rtac conjI 1);
-by (assume_tac 2);
-by (rtac conjunct1 1);
-by (assume_tac 1);
-result();
-
-(*A form of conj-elimination*)
-val prems = 
-goal IFOL.thy "A&B ==> ([| A;  B |] ==> C) ==> C";
-by (resolve_tac prems 1);
-by (rtac conjunct1 1);
-by (resolve_tac prems 1);
-by (rtac conjunct2 1);
-by (resolve_tac prems 1);
-result();
-
-
-val prems = 
-goal IFOL.thy "(!!A. ~ ~A ==> A) ==> B | ~B";
-by (resolve_tac prems 1);
-by (rtac notI 1);
-by (res_inst_tac [ ("P", "~B") ]  notE  1);
-by (rtac notI 2);
-by (res_inst_tac [ ("P", "B | ~B") ]  notE  2);
-by (assume_tac 2);
-by (rtac disjI1 2);
-by (assume_tac 2);
-by (rtac notI 1);
-by (res_inst_tac [ ("P", "B | ~B") ]  notE  1);
-by (assume_tac 1);
-by (rtac disjI2 1);
-by (assume_tac 1);
-result();
-
-
-val prems = 
-goal IFOL.thy "(!!A. ~ ~A ==> A) ==> B | ~B";
-by (resolve_tac prems 1);
-by (rtac notI 1);
-by (rtac notE 1);
-by (rtac notI 2);
-by (etac notE 2);
-by (etac disjI1 2);
-by (rtac notI 1);
-by (etac notE 1);
-by (etac disjI2 1);
-result();
-
-
-val prems = 
-goal IFOL.thy "[| A | ~A;  ~ ~A |] ==> A";
-by (rtac disjE 1);
-by (resolve_tac prems 1);
-by (assume_tac 1);
-by (rtac FalseE 1);
-by (res_inst_tac [ ("P", "~A") ]  notE  1);
-by (resolve_tac prems 1);
-by (assume_tac 1);
-result();
-
-
-writeln"Examples with quantifiers";
-
-val prems =
-goal IFOL.thy "ALL z. G(z) ==> ALL z. G(z)|H(z)";
-by (rtac allI 1);
-by (rtac disjI1 1);
-by (resolve_tac (prems RL [spec]) 1); 
-  (*can use instead
-    by (rtac spec 1);  by (resolve_tac prems 1); *)
-result();
-
-
-goal IFOL.thy "ALL x. EX y. x=y";
-by (rtac allI 1);
-by (rtac exI 1);
-by (rtac refl 1);
-result();
-
-
-goal IFOL.thy "EX y. ALL x. x=y";
-by (rtac exI 1);
-by (rtac allI 1);
-by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected";  
-getgoal 1; 
-
-
-(*Parallel lifting example. *)
-goal IFOL.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
-by (resolve_tac [exI, allI] 1);
-by (resolve_tac [exI, allI] 1);
-by (resolve_tac [exI, allI] 1);
-by (resolve_tac [exI, allI] 1);
-by (resolve_tac [exI, allI] 1);
-
-
-val prems =
-goal IFOL.thy "(EX z. F(z)) & B ==> (EX z. F(z) & B)";
-by (rtac conjE 1);
-by (resolve_tac prems 1);
-by (rtac exE 1);
-by (assume_tac 1);
-by (rtac exI 1);
-by (rtac conjI 1);
-by (assume_tac 1);
-by (assume_tac 1);
-result();
-
-
-(*A bigger demonstration of quantifiers -- not in the paper*)
-goal IFOL.thy "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
-by (rtac impI 1);
-by (rtac allI 1);
-by (rtac exE 1 THEN assume_tac 1);
-by (rtac exI 1);
-by (rtac allE 1 THEN assume_tac 1);
-by (assume_tac 1);
-result();  

--- a/src/FOL/ex/intro.ML	Wed Jun 07 16:55:39 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(*  Title:      FOL/ex/intro
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Examples for the manual "Introduction to Isabelle"
-
-Derives some inference rules, illustrating the use of definitions
-
-To generate similar output to manual, execute these commands:
-    Pretty.setmargin 72; print_depth 0;
-*)
-
-
-context FOL.thy;
-
-(**** Some simple backward proofs ****)
-
-Goal "P|P --> P";
-by (rtac impI 1);
-by (rtac disjE 1);
-by (assume_tac 3);
-by (assume_tac 2);
-by (assume_tac 1);
-qed "mythm";
-
-Goal "(P & Q) | R  --> (P | R)";
-by (rtac impI 1);
-by (etac disjE 1);
-by (dtac conjunct1 1);
-by (rtac disjI1 1);
-by (rtac disjI2 2);
-by (REPEAT (assume_tac 1));
-result();
-
-(*Correct version, delaying use of "spec" until last*)
-Goal "(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
-by (rtac impI 1);
-by (rtac allI 1);
-by (rtac allI 1);
-by (dtac spec 1);
-by (dtac spec 1);
-by (assume_tac 1);
-result();
-
-
-(**** Demonstration of Fast_tac ****)
-
-Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
-\       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
-by (Fast_tac 1);
-result();
-
-Goal "ALL x. P(x,f(x)) <-> \
-\       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
-by (Fast_tac 1);
-result();
-
-
-(**** Derivation of conjunction elimination rule ****)
-
-val [major,minor] = Goal "[| P&Q;  [| P; Q |] ==> R |] ==> R";
-by (rtac minor 1);
-by (resolve_tac [major RS conjunct1] 1);
-by (resolve_tac [major RS conjunct2] 1);
-prth (topthm());
-result();
-
-
-(**** Derived rules involving definitions ****)
-
-(** Derivation of negation introduction **)
-
-val prems = Goal "(P ==> False) ==> ~P";
-by (rewtac not_def);
-by (rtac impI 1);
-by (resolve_tac prems 1);
-by (assume_tac 1);
-result();
-
-val [major,minor] = goal FOL.thy "[| ~P;  P |] ==> R";
-by (rtac FalseE 1);
-by (rtac mp 1);
-by (resolve_tac [rewrite_rule [not_def] major] 1);
-by (rtac minor 1);
-result();
-
-(*Alternative proof of the result above*)
-val [major,minor] = goalw FOL.thy [not_def]
-    "[| ~P;  P |] ==> R";
-by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
-result();
-
-writeln"Reached end of file.";