# HG changeset patch
# User wenzelm
# Date 1201460672 -3600
# Node ID 31b38a39e58978ce0912c20d8b41056b3b7e50a4
# Parent  d98da4a40a796de80fe6ce5803449643349c609a
eliminated some legacy ML files;

diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/IsaMakefile
--- a/src/FOLP/IsaMakefile	Sun Jan 27 20:04:31 2008 +0100
+++ b/src/FOLP/IsaMakefile	Sun Jan 27 20:04:32 2008 +0100
@@ -35,8 +35,8 @@
 
 FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
 
-$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/foundn.ML \
-  ex/If.ML ex/If.thy ex/int.ML ex/intro.ML ex/Nat.ML ex/Nat.thy \
+$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/Foundation.thy \
+  ex/If.thy ex/int.ML ex/Intro.thy ex/Nat.thy \
   ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
 	@$(ISATOOL) usedir $(OUT)/FOLP ex
 
diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/ex/Foundation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOLP/ex/Foundation.thy	Sun Jan 27 20:04:32 2008 +0100
@@ -0,0 +1,135 @@
+(*  Title:      FOLP/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 IFOLP
+begin
+
+lemma "?p : 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 "p : A & B"
+    and "!!x y. x : A ==> y : B ==> f(x, y) : C"
+  shows "?p : C"
+apply (rule prems)
+apply (rule conjunct1)
+apply (rule prems)
+apply (rule conjunct2)
+apply (rule prems)
+done
+
+lemma
+  assumes "!!A x. x : ~ ~A ==> cla(x) : A"
+  shows "?p : 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 x. x : ~ ~A ==> cla(x) : A"
+  shows "?p : 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 "p : A | ~A"
+    and "q : ~ ~A"
+  shows "?p : 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 "p : ALL z. G(z)"
+  shows "?p : ALL z. G(z)|H(z)"
+apply (rule allI)
+apply (rule disjI1)
+apply (rule prems [THEN spec])
+done
+
+lemma "?p : ALL x. EX y. x=y"
+apply (rule allI)
+apply (rule exI)
+apply (rule refl)
+done
+
+lemma "?p : EX y. ALL x. x=y"
+apply (rule exI)
+apply (rule allI)
+apply (rule refl)?
+oops
+
+text {* Parallel lifting example. *}
+lemma "?p : 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 "p : (EX z. F(z)) & B"
+  shows "?p : 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 "?p : (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
diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/ex/If.ML
--- a/src/FOLP/ex/If.ML	Sun Jan 27 20:04:31 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      FOLP/ex/If.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-*)
-
-val prems = goalw (the_context ()) [if_def]
-    "[| !!x. x:P ==> f(x):Q; !!x. x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
-by (fast_tac (FOLP_cs addIs prems) 1);
-val ifI = result();
-
-val major::prems = goalw (the_context ()) [if_def]
-   "[| p:if(P,Q,R);  !!x y.[| x:P; y:Q |] ==> f(x,y):S; \
-\                    !!x y.[| x:~P; y:R |] ==> g(x,y):S |] ==> ?p:S";
-by (cut_facts_tac [major] 1);
-by (fast_tac (FOLP_cs addIs prems) 1);
-val ifE = result();
-
-
-Goal
-    "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
-by (rtac iffI 1);
-by (etac ifE 1);
-by (etac ifE 1);
-by (rtac ifI 1);
-by (rtac ifI 1);
-
-choplev 0;
-val if_cs = FOLP_cs addSIs [ifI] addSEs[ifE];
-by (fast_tac if_cs 1);
-val if_commute = result();
-
-
-Goal "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
-by (fast_tac if_cs 1);
-val nested_ifs = result();
diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/ex/If.thy
--- a/src/FOLP/ex/If.thy	Sun Jan 27 20:04:31 2008 +0100
+++ b/src/FOLP/ex/If.thy	Sun Jan 27 20:04:32 2008 +0100
@@ -8,6 +8,39 @@
   "if" :: "[o,o,o]=>o"
   "if(P,Q,R) == P&Q | ~P&R"
 
-ML {* use_legacy_bindings (the_context ()) *}
+lemma ifI:
+  assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
+  shows "?p : if(P,Q,R)"
+apply (unfold if_def)
+apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
+done
+
+lemma ifE:
+  assumes 1: "p : if(P,Q,R)" and
+    2: "!!x y. [| x : P; y : Q |] ==> f(x, y) : S" and
+    3: "!!x y. [| x : ~P; y : R |] ==> g(x, y) : S"
+  shows "?p : S"
+apply (insert 1)
+apply (unfold if_def)
+apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
+done
+
+lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
+apply (rule iffI)
+apply (erule ifE)
+apply (erule ifE)
+apply (rule ifI)
+apply (rule ifI)
+oops
+
+ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
+
+lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
+apply (tactic {* fast_tac if_cs 1 *})
+done
+
+lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
+apply (tactic {* fast_tac if_cs 1 *})
+done
 
 end
diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/ex/Intro.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOLP/ex/Intro.thy	Sun Jan 27 20:04:32 2008 +0100
@@ -0,0 +1,102 @@
+(*  Title:      FOLP/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 FOLP
+begin
+
+subsubsection {* Some simple backward proofs *}
+
+lemma mythm: "?p : P|P --> P"
+apply (rule impI)
+apply (rule disjE)
+prefer 3 apply (assumption)
+prefer 2 apply (assumption)
+apply assumption
+done
+
+lemma "?p : (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 "?p : (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 "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
+        -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
+apply (tactic {* fast_tac FOLP_cs 1 *})
+done
+
+
+lemma "?p : ALL x. P(x,f(x)) <->
+        (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
+apply (tactic {* fast_tac FOLP_cs 1 *})
+done
+
+
+subsubsection {* Derivation of conjunction elimination rule *}
+
+lemma
+  assumes major: "p : P&Q"
+    and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R"
+  shows "?p : 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 "!!x. x : P ==> f(x) : False"
+  shows "?p : ~ P"
+apply (unfold not_def)
+apply (rule impI)
+apply (rule prems)
+apply assumption
+done
+
+lemma
+  assumes major: "p : ~P"
+    and minor: "q : P"
+  shows "?p : 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 : ~P"
+    and minor: "q : P"
+  shows "?p : R"
+apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])
+done
+
+end
diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/ex/Nat.ML
--- a/src/FOLP/ex/Nat.ML	Sun Jan 27 20:04:31 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(*  Title:      FOLP/ex/Nat.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-*)
-
-Goal "?p : ~ (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);
-val Suc_n_not_n = result();
-
-
-Goal "?p : (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] "?p : 0+n = n";
-by (rtac rec_0 1);
-val add_0 = result();
-
-Goalw [add_def] "?p : Suc(m)+n = Suc(m+n)";
-by (rtac rec_Suc 1);
-val add_Suc = result();
-
-(*
-val nat_congs = mk_congs (the_context ()) ["Suc", "op +"];
-prths nat_congs;
-*)
-val prems = goal (the_context ()) "p: x=y ==> ?p : Suc(x) = Suc(y)";
-by (resolve_tac (prems RL [subst]) 1);
-by (rtac refl 1);
-val Suc_cong = result();
-
-val prems = goal (the_context ()) "[| p : a=x;  q: b=y |] ==> ?p : a+b=x+y";
-by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN
-    rtac refl 1);
-val Plus_cong = result();
-
-val nat_congs = [Suc_cong,Plus_cong];
-
-
-val add_ss = FOLP_ss  addcongs nat_congs
-                     addrews  [add_0, add_Suc];
-
-Goal "?p : (k+m)+n = k+(m+n)";
-by (res_inst_tac [("n","k")] induct 1);
-by (SIMP_TAC add_ss 1);
-by (ASM_SIMP_TAC add_ss 1);
-val add_assoc = result();
-
-Goal "?p : m+0 = m";
-by (res_inst_tac [("n","m")] induct 1);
-by (SIMP_TAC add_ss 1);
-by (ASM_SIMP_TAC add_ss 1);
-val add_0_right = result();
-
-Goal "?p : m+Suc(n) = Suc(m+n)";
-by (res_inst_tac [("n","m")] induct 1);
-by (ALLGOALS (ASM_SIMP_TAC add_ss));
-val add_Suc_right = result();
-
-(*mk_typed_congs appears not to work with FOLP's version of subst*)
diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Sun Jan 27 20:04:31 2008 +0100
+++ b/src/FOLP/ex/Nat.thy	Sun Jan 27 20:04:32 2008 +0100
@@ -11,18 +11,20 @@
 begin
 
 typedecl nat
-arities nat         :: "term"
-consts  "0"         :: "nat"    ("0")
-        Suc         :: "nat=>nat"
-        rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
-        "+"         :: "[nat, nat] => nat"              (infixl 60)
+arities nat :: "term"
+
+consts
+  0 :: nat    ("0")
+  Suc :: "nat => nat"
+  rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
+  add :: "[nat, nat] => nat"    (infixl "+" 60)
 
   (*Proof terms*)
-       nrec         :: "[nat,p,[nat,p]=>p]=>p"
-       ninj         :: "p=>p"
-       nneq         :: "p=>p"
-       rec0         :: "p"
-       recSuc       :: "p"
+  nrec :: "[nat, p, [nat, p] => p] => p"
+  ninj :: "p => p"
+  nneq :: "p => p"
+  rec0 :: "p"
+  recSuc :: "p"
 
 axioms
   induct:     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
@@ -32,11 +34,79 @@
   Suc_neq_0:  "p:Suc(m)=0      ==> nneq(p) : R"
   rec_0:      "rec0 : rec(0,a,f) = a"
   rec_Suc:    "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
+
+defs
   add_def:    "m+n == rec(m, n, %x y. Suc(y))"
 
+axioms
   nrecB0:     "b: A ==> nrec(0,b,c) = b : A"
   nrecBSuc:   "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+subsection {* Proofs about the natural numbers *}
+
+lemma Suc_n_not_n: "?p : ~ (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 "?p : (k+m)+n = k+(m+n)"
+apply (rule induct)
+back
+back
+back
+back
+back
+back
+oops
+
+lemma add_0 [simp]: "?p : 0+n = n"
+apply (unfold add_def)
+apply (rule rec_0)
+done
+
+lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
+apply (unfold add_def)
+apply (rule rec_Suc)
+done
+
+
+lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
+  apply (erule subst)
+  apply (rule refl)
+  done
+
+lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
+  apply (erule subst, erule subst, rule refl)
+  done
+
+lemmas nat_congs = Suc_cong Plus_cong
+
+ML {*
+  val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
+*}
+
+lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
+apply (rule_tac n = k in induct)
+apply (tactic {* SIMP_TAC add_ss 1 *})
+apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
+done
+
+lemma add_0_right: "?p : m+0 = m"
+apply (rule_tac n = m in induct)
+apply (tactic {* SIMP_TAC add_ss 1 *})
+apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
+done
+
+lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
+apply (rule_tac n = m in induct)
+apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
+done
+
+(*mk_typed_congs appears not to work with FOLP's version of subst*)
 
 end
diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/ex/ROOT.ML
--- a/src/FOLP/ex/ROOT.ML	Sun Jan 27 20:04:31 2008 +0100
+++ b/src/FOLP/ex/ROOT.ML	Sun Jan 27 20:04:32 2008 +0100
@@ -6,9 +6,12 @@
 Examples for First-Order Logic. 
 *)
 
-time_use     "intro.ML";
-time_use_thy "Nat";
-time_use     "foundn.ML";
+use_thys [
+  "Intro",
+  "Nat",
+  "Foundation",
+  "If"
+];
 
 writeln"\n** Intuitionistic examples **\n";
 time_use     "int.ML";
@@ -19,7 +22,6 @@
 
 writeln"\n** Classical examples **\n";
 time_use     "cla.ML";
-time_use_thy "If";
 
 val thy = theory "FOLP"  and  tac = Cla.fast_tac FOLP_cs 1;
 time_use     "prop.ML";
diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/ex/foundn.ML
--- a/src/FOLP/ex/foundn.ML	Sun Jan 27 20:04:31 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-(*  Title:      FOLP/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 (theory "IFOLP") "?p : 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 (theory "IFOLP") "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p: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 (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p: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 (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p: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 (theory "IFOLP") "[| p:A | ~A;  q:~ ~A |] ==> ?p: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 (theory "IFOLP") "p : ALL z. G(z) ==> ?p: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 (theory "IFOLP") "?p : ALL x. EX y. x=y";
-by (rtac allI 1);
-by (rtac exI 1);
-by (rtac refl 1);
-result();
-
-
-goal (theory "IFOLP") "?p : 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 (theory "IFOLP") "?p : 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 (theory "IFOLP") "p : (EX z. F(z)) & B ==> ?p:(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 (theory "IFOLP") "?p : (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();  
diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/ex/intro.ML
--- a/src/FOLP/ex/intro.ML	Sun Jan 27 20:04:31 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-(*  Title:      FOLP/ex/intro.ML
-    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;
-*)
-
-
-(**** Some simple backward proofs ****)
-
-goal (theory "FOLP") "?p:P|P --> P";
-by (rtac impI 1);
-by (rtac disjE 1);
-by (assume_tac 3);
-by (assume_tac 2);
-by (assume_tac 1);
-val mythm = result();
-
-goal (theory "FOLP") "?p:(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 (theory "FOLP") "?p:(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 (theory "FOLP") "?p:(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 FOLP_cs 1);
-result();
-
-goal (theory "FOLP") "?p:ALL x. P(x,f(x)) <-> \
-\       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
-by (fast_tac FOLP_cs 1);
-result();
-
-
-(**** Derivation of conjunction elimination rule ****)
-
-val [major,minor] = goal (theory "FOLP") "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p: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 (theory "FOLP") "(!!x. x:P ==> f(x):False) ==> ?p:~P";
-by (rewtac not_def);
-by (rtac impI 1);
-by (resolve_tac prems 1);
-by (assume_tac 1);
-result();
-
-val [major,minor] = goal (theory "FOLP") "[| p:~P;  q: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 above result*)
-val [major,minor] = goalw (theory "FOLP") [not_def]
-    "[| p:~P;  q:P |] ==> ?p:R";
-by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
-result();
diff -r d98da4a40a79 -r 31b38a39e589 src/FOLP/ex/prop.ML
--- a/src/FOLP/ex/prop.ML	Sun Jan 27 20:04:31 2008 +0100
+++ b/src/FOLP/ex/prop.ML	Sun Jan 27 20:04:32 2008 +0100
@@ -7,6 +7,9 @@
 Needs declarations of the theory "thy" and the tactic "tac"
 *)
 
+ML_Context.set_context (SOME (Context.Theory thy));
+
+
 writeln"commutative laws of & and | ";
 Goal "?p : P & Q  -->  Q & P";
 by tac;