# HG changeset patch
# User wenzelm
# Date 1127046348 -7200
# Node ID fd19f77dcf6003bafc64c130d7b8bfee825ff687
# Parent  68a7acb5f22ebb1d3accb4f9a2d9f6a252a2daa9
converted to Isar theory format;

diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/FOLP.ML
--- a/src/FOLP/FOLP.ML	Sat Sep 17 20:49:14 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-(*  Title:      FOLP/FOLP.ML
-    ID:         $Id$
-    Author:     Martin D Coen, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Tactics and lemmas for FOLP (Classical First-Order Logic with Proofs)
-*)
-
-(*** Classical introduction rules for | and EX ***)
-
-val prems= goal FOLP.thy 
-   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
-by (rtac classical 1);
-by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
-by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
-qed "disjCI";
-
-(*introduction rule involving only EX*)
-val prems= goal FOLP.thy 
-   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
-by (rtac classical 1);
-by (eresolve_tac (prems RL [exI]) 1) ;
-qed "ex_classical";
-
-(*version of above, simplifying ~EX to ALL~ *)
-val [prem]= goal FOLP.thy 
-   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
-by (rtac ex_classical 1);
-by (resolve_tac [notI RS allI RS prem] 1);
-by (etac notE 1);
-by (etac exI 1) ;
-qed "exCI";
-
-val excluded_middle = prove_goal FOLP.thy "?p : ~P | P"
- (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
-
-
-(*** Special elimination rules *)
-
-
-(*Classical implies (-->) elimination. *)
-val major::prems= goal FOLP.thy 
-    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R";
-by (resolve_tac [excluded_middle RS disjE] 1);
-by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
-qed "impCE";
-
-(*Double negation law*)
-Goal "p:~~P ==> ?p : P";
-by (rtac classical 1);
-by (etac notE 1);
-by (assume_tac 1);
-qed "notnotD";
-
-
-(*** Tactics for implication and contradiction ***)
-
-(*Classical <-> elimination.  Proof substitutes P=Q in 
-    ~P ==> ~Q    and    P ==> Q  *)
-val prems = goalw FOLP.thy [iff_def]
-    "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
-\                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
-by (rtac conjE 1);
-by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
-               ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ;
-qed "iffCE";
-
-
-(*Should be used as swap since ~P becomes redundant*)
-val major::prems= goal FOLP.thy 
-   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
-by (rtac classical 1);
-by (rtac (major RS notE) 1);
-by (REPEAT (ares_tac prems 1)) ;
-qed "swap";
-
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/FOLP.thy
--- a/src/FOLP/FOLP.thy	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/FOLP.thy	Sun Sep 18 14:25:48 2005 +0200
@@ -2,13 +2,88 @@
     ID:         $Id$
     Author:     Martin D Coen, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
-Classical First-Order Logic with Proofs
 *)
 
-FOLP = IFOLP +
+header {* Classical First-Order Logic with Proofs *}
+
+theory FOLP
+imports IFOLP
+uses
+  ("FOLP_lemmas.ML") ("hypsubst.ML") ("classical.ML")
+  ("simp.ML") ("intprover.ML") ("simpdata.ML")
+begin
+
 consts
   cla :: "[p=>p]=>p"
-rules
-  classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
+axioms
+  classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
+use "FOLP_lemmas.ML"
+
+use "hypsubst.ML"
+use "classical.ML"      (* Patched 'cos matching won't instantiate proof *)
+use "simp.ML"           (* Patched 'cos matching won't instantiate proof *)
+
+ML {*
+
+(*** Applying HypsubstFun to generate hyp_subst_tac ***)
+
+structure Hypsubst_Data =
+  struct
+  (*Take apart an equality judgement; otherwise raise Match!*)
+  fun dest_eq (Const("Proof",_) $ (Const("op =",_)  $ t $ u) $ _) = (t,u);
+
+  val imp_intr = impI
+
+  (*etac rev_cut_eq moves an equality to be the last premise. *)
+  val rev_cut_eq = prove_goal (the_context ())
+                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
+   (fn prems => [ REPEAT(resolve_tac prems 1) ]);
+
+  val rev_mp = rev_mp
+  val subst = subst
+  val sym = sym
+  val thin_refl = prove_goal (the_context ())
+                  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
+  end;
+
+structure Hypsubst = HypsubstFun(Hypsubst_Data);
+open Hypsubst;
+*}
+
+use "intprover.ML"
+
+ML {*
+(*** Applying ClassicalFun to create a classical prover ***)
+structure Classical_Data =
+  struct
+  val sizef = size_of_thm
+  val mp = mp
+  val not_elim = notE
+  val swap = swap
+  val hyp_subst_tacs=[hyp_subst_tac]
+  end;
+
+structure Cla = ClassicalFun(Classical_Data);
+open Cla;
+
+(*Propositional rules
+  -- iffCE might seem better, but in the examples in ex/cla
+     run about 7% slower than with iffE*)
+val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
+                       addSEs [conjE,disjE,impCE,FalseE,iffE];
+
+(*Quantifier rules*)
+val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
+                      addSEs [exE,ex1E] addEs [allE];
+
+val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]
+                          addSEs [exE,ex1E] addEs [all_dupE];
+
+*}
+
+use "simpdata.ML"
+
 end
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/FOLP_lemmas.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOLP/FOLP_lemmas.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -0,0 +1,73 @@
+(*  Title:      FOLP/FOLP.ML
+    ID:         $Id$
+    Author:     Martin D Coen, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+*)
+
+(*** Classical introduction rules for | and EX ***)
+
+val prems= goal (the_context ())
+   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
+by (rtac classical 1);
+by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
+by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
+qed "disjCI";
+
+(*introduction rule involving only EX*)
+val prems= goal (the_context ())
+   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
+by (rtac classical 1);
+by (eresolve_tac (prems RL [exI]) 1) ;
+qed "ex_classical";
+
+(*version of above, simplifying ~EX to ALL~ *)
+val [prem]= goal (the_context ())
+   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
+by (rtac ex_classical 1);
+by (resolve_tac [notI RS allI RS prem] 1);
+by (etac notE 1);
+by (etac exI 1) ;
+qed "exCI";
+
+val excluded_middle = prove_goal (the_context ()) "?p : ~P | P"
+ (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
+
+
+(*** Special elimination rules *)
+
+
+(*Classical implies (-->) elimination. *)
+val major::prems= goal (the_context ())
+    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R";
+by (resolve_tac [excluded_middle RS disjE] 1);
+by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
+qed "impCE";
+
+(*Double negation law*)
+Goal "p:~~P ==> ?p : P";
+by (rtac classical 1);
+by (etac notE 1);
+by (assume_tac 1);
+qed "notnotD";
+
+
+(*** Tactics for implication and contradiction ***)
+
+(*Classical <-> elimination.  Proof substitutes P=Q in
+    ~P ==> ~Q    and    P ==> Q  *)
+val prems = goalw (the_context ()) [iff_def]
+    "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
+\                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
+by (rtac conjE 1);
+by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
+               ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ;
+qed "iffCE";
+
+
+(*Should be used as swap since ~P becomes redundant*)
+val major::prems= goal (the_context ())
+   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
+by (rtac classical 1);
+by (rtac (major RS notE) 1);
+by (REPEAT (ares_tac prems 1)) ;
+qed "swap";
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/IFOLP.ML
--- a/src/FOLP/IFOLP.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/IFOLP.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -2,29 +2,28 @@
     ID:         $Id$
     Author:     Martin D Coen, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
+*)
 
-Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs)
-*)
 (*** Sequent-style elimination rules for & --> and ALL ***)
 
-val prems= Goal 
+val prems= Goal
     "[| p:P&Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R |] ==> ?a:R";
 by (REPEAT (resolve_tac prems 1
    ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN resolve_tac prems 1))) ;
 qed "conjE";
 
-val prems= Goal 
+val prems= Goal
     "[| p:P-->Q;  q:P;  !!x. x:Q ==> r(x):R |] ==> ?p:R";
 by (REPEAT (resolve_tac (prems@[mp]) 1)) ;
 qed "impE";
 
-val prems= Goal 
+val prems= Goal
     "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R";
 by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
 qed "allE";
 
 (*Duplicates the quantifier; for use with eresolve_tac*)
-val prems= Goal 
+val prems= Goal
     "[| p:ALL x. P(x);  !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
 \    |] ==> ?p:R";
 by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
@@ -33,16 +32,16 @@
 
 (*** Negation rules, which translate between ~P and P-->False ***)
 
-val notI = prove_goalw IFOLP.thy [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
+val notI = prove_goalw (the_context ()) [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
  (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
 
-val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P;  q:P |] ==> ?p:R"
+val notE = prove_goalw (the_context ()) [not_def] "[| p:~P;  q:P |] ==> ?p:R"
  (fn prems=>
   [ (resolve_tac [mp RS FalseE] 1),
     (REPEAT (resolve_tac prems 1)) ]);
 
 (*This is useful with the special implication rules for each kind of P. *)
-val prems= Goal 
+val prems= Goal
     "[| p:~P;  !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q";
 by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ;
 qed "not_to_imp";
@@ -65,7 +64,7 @@
 
 (** Unique assumption tactic.
     Ignores proof objects.
-    Fails unless one assumption is equal and exactly one is unifiable 
+    Fails unless one assumption is equal and exactly one is unifiable
 **)
 
 local
@@ -76,7 +75,7 @@
     (fn (prem,i) =>
       let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
           and concl = discard_proof (Logic.strip_assums_concl prem)
-      in  
+      in
           if exists (fn hyp => hyp aconv concl) hyps
           then case distinct (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
                    [_] => assume_tac i
@@ -97,22 +96,22 @@
 
 (*** If-and-only-if ***)
 
-val iffI = prove_goalw IFOLP.thy [iff_def]
+val iffI = prove_goalw (the_context ()) [iff_def]
    "[| !!x. x:P ==> q(x):Q;  !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q"
  (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);
 
 
 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
-val iffE = prove_goalw IFOLP.thy [iff_def]
+val iffE = prove_goalw (the_context ()) [iff_def]
     "[| p:P <-> Q;  !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R"
  (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]);
 
 (* Destruct rules for <-> similar to Modus Ponens *)
 
-val iffD1 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q;  q:P |] ==> ?p:Q"
+val iffD1 = prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q;  q:P |] ==> ?p:Q"
  (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
 
-val iffD2 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q;  q:Q |] ==> ?p:P"
+val iffD2 = prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q;  q:Q |] ==> ?p:P"
  (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
 
 Goal "?p:P <-> P";
@@ -137,12 +136,12 @@
  do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
 ***)
 
-val prems = goalw IFOLP.thy [ex1_def]
+val prems = goalw (the_context ()) [ex1_def]
     "[| p:P(a);  !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)";
 by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ;
 qed "ex1I";
 
-val prems = goalw IFOLP.thy [ex1_def]
+val prems = goalw (the_context ()) [ex1_def]
     "[| p:EX! x. P(x);  \
 \       !!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
 \    ?a : R";
@@ -158,7 +157,7 @@
     resolve_tac (prems RL [iffE]) i THEN
     REPEAT1 (eresolve_tac [asm_rl,mp] i);
 
-val conj_cong = prove_goal IFOLP.thy 
+val conj_cong = prove_goal (the_context ())
     "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
  (fn prems =>
   [ (cut_facts_tac prems 1),
@@ -166,7 +165,7 @@
       ORELSE  eresolve_tac [iffE,conjE,mp] 1
       ORELSE  iff_tac prems 1)) ]);
 
-val disj_cong = prove_goal IFOLP.thy 
+val disj_cong = prove_goal (the_context ())
     "[| p:P <-> P';  q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
  (fn prems =>
   [ (cut_facts_tac prems 1),
@@ -174,7 +173,7 @@
       ORELSE  ares_tac [iffI] 1
       ORELSE  mp_tac 1)) ]);
 
-val imp_cong = prove_goal IFOLP.thy 
+val imp_cong = prove_goal (the_context ())
     "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
  (fn prems =>
   [ (cut_facts_tac prems 1),
@@ -182,7 +181,7 @@
       ORELSE  etac iffE 1
       ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]);
 
-val iff_cong = prove_goal IFOLP.thy 
+val iff_cong = prove_goal (the_context ())
     "[| p:P <-> P';  q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
  (fn prems =>
   [ (cut_facts_tac prems 1),
@@ -190,7 +189,7 @@
       ORELSE  ares_tac [iffI] 1
       ORELSE  mp_tac 1)) ]);
 
-val not_cong = prove_goal IFOLP.thy 
+val not_cong = prove_goal (the_context ())
     "p:P <-> P' ==> ?p:~P <-> ~P'"
  (fn prems =>
   [ (cut_facts_tac prems 1),
@@ -198,14 +197,14 @@
       ORELSE  mp_tac 1
       ORELSE  eresolve_tac [iffE,notE] 1)) ]);
 
-val all_cong = prove_goal IFOLP.thy 
+val all_cong = prove_goal (the_context ())
     "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
  (fn prems =>
   [ (REPEAT   (ares_tac [iffI,allI] 1
       ORELSE   mp_tac 1
       ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
 
-val ex_cong = prove_goal IFOLP.thy 
+val ex_cong = prove_goal (the_context ())
     "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))"
  (fn prems =>
   [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
@@ -213,7 +212,7 @@
       ORELSE   iff_tac prems 1)) ]);
 
 (*NOT PROVED
-val ex1_cong = prove_goal IFOLP.thy 
+val ex1_cong = prove_goal (the_context ())
     "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
  (fn prems =>
   [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
@@ -225,8 +224,8 @@
 
 val refl = ieqI;
 
-val subst = prove_goal IFOLP.thy "[| p:a=b;  q:P(a) |] ==> ?p : P(b)"
- (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1), 
+val subst = prove_goal (the_context ()) "[| p:a=b;  q:P(a) |] ==> ?p : P(b)"
+ (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1),
                         rtac impI 1, atac 1 ]);
 
 Goal "q:a=b ==> ?c:b=a";
@@ -235,7 +234,7 @@
 qed "sym";
 
 Goal "[| p:a=b;  q:b=c |] ==> ?d:a=c";
-by (etac subst 1 THEN assume_tac 1); 
+by (etac subst 1 THEN assume_tac 1);
 qed "trans";
 
 (** ~ b=a ==> ~ a=b **)
@@ -263,12 +262,12 @@
 qed "subst_context";
 
 Goal "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)";
-by (REPEAT (etac ssubst 1)); 
+by (REPEAT (etac ssubst 1));
 by (rtac refl 1) ;
 qed "subst_context2";
 
 Goal "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)";
-by (REPEAT (etac ssubst 1)); 
+by (REPEAT (etac ssubst 1));
 by (rtac refl 1) ;
 qed "subst_context3";
 
@@ -309,8 +308,8 @@
 
 (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
 
-val pred_congs = 
-    List.concat (map (fn c => 
+val pred_congs =
+    List.concat (map (fn c =>
                map (fn th => read_instantiate [("P",c)] th)
                    [pred1_cong,pred2_cong,pred3_cong])
                (explode"PQRS"));
@@ -321,30 +320,30 @@
 
 (*** Simplifications of assumed implications.
      Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
-     used with mp_tac (restricted to atomic formulae) is COMPLETE for 
+     used with mp_tac (restricted to atomic formulae) is COMPLETE for
      intuitionistic propositional logic.  See
    R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
     (preprint, University of St Andrews, 1991)  ***)
 
-val major::prems= Goal 
+val major::prems= Goal
     "[| p:(P&Q)-->S;  !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R";
 by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ;
 qed "conj_impE";
 
-val major::prems= Goal 
+val major::prems= Goal
     "[| p:(P|Q)-->S;  !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R";
 by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ;
 qed "disj_impE";
 
-(*Simplifies the implication.  Classical version is stronger. 
+(*Simplifies the implication.  Classical version is stronger.
   Still UNSAFE since Q must be provable -- backtracking needed.  *)
-val major::prems= Goal 
+val major::prems= Goal
     "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x. x:S ==> r(x):R |] ==> \
 \    ?p:R";
 by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ;
 qed "imp_impE";
 
-(*Simplifies the implication.  Classical version is stronger. 
+(*Simplifies the implication.  Classical version is stronger.
   Still UNSAFE since ~P must be provable -- backtracking needed.  *)
 val major::prems= Goal
     "[| p:~P --> S;  !!y. y:P ==> q(y):False;  !!y. y:S ==> r(y):R |] ==> ?p:R";
@@ -352,20 +351,20 @@
 qed "not_impE";
 
 (*Simplifies the implication.   UNSAFE.  *)
-val major::prems= Goal 
+val major::prems= Goal
     "[| p:(P<->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  \
 \       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x. x:S ==> s(x):R |] ==> ?p:R";
 by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ;
 qed "iff_impE";
 
 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
-val major::prems= Goal 
+val major::prems= Goal
     "[| p:(ALL x. P(x))-->S;  !!x. q:P(x);  !!y. y:S ==> r(y):R |] ==> ?p:R";
 by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ;
 qed "all_impE";
 
 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
-val major::prems= Goal 
+val major::prems= Goal
     "[| p:(EX x. P(x))-->S;  !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R";
 by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ;
 qed "ex_impE";
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/IFOLP.thy	Sun Sep 18 14:25:48 2005 +0200
@@ -2,30 +2,32 @@
     ID:         $Id$
     Author:     Martin D Coen, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
-Intuitionistic First-Order Logic with Proofs
 *)
 
-IFOLP = Pure +
+header {* Intuitionistic First-Order Logic with Proofs *}
+
+theory IFOLP
+imports Pure
+begin
 
 global
 
-classes term
-default term
+classes "term"
+defaultsort "term"
 
-types
-  p
-  o
+typedecl p
+typedecl o
 
-consts  
+consts
       (*** Judgements ***)
  "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
  Proof          ::   "[o,p]=>prop"
  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
-        
+
       (*** Logical Connectives -- Type Formers ***)
  "="            ::      "['a,'a] => o"  (infixl 50)
- True,False     ::      "o"
+ True           ::      "o"
+ False          ::      "o"
  Not            ::      "o => o"        ("~ _" [40] 40)
  "&"            ::      "[o,o] => o"    (infixr 35)
  "|"            ::      "[o,o] => o"    (infixr 30)
@@ -42,10 +44,12 @@
       (*** Proof Term Formers: precedence must exceed 50 ***)
  tt             :: "p"
  contr          :: "p=>p"
- fst,snd        :: "p=>p"
+ fst            :: "p=>p"
+ snd            :: "p=>p"
  pair           :: "[p,p]=>p"           ("(1<_,/_>)")
  split          :: "[p, [p,p]=>p] =>p"
- inl,inr        :: "p=>p"
+ inl            :: "p=>p"
+ inr            :: "p=>p"
  when           :: "[p, p=>p, p=>p]=>p"
  lambda         :: "(p => p) => p"      (binder "lam " 55)
  "`"            :: "[p,p]=>p"           (infixl 60)
@@ -55,98 +59,103 @@
  xsplit         :: "[p,['a,p]=>p]=>p"
  ideq           :: "'a=>p"
  idpeel         :: "[p,'a=>p]=>p"
- nrm, NRM       :: "p"
+ nrm            :: p
+ NRM            :: p
 
 local
 
-rules
+ML {*
+
+(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
+val show_proofs = ref false;
+
+fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
+
+fun proof_tr' [P,p] =
+    if !show_proofs then Const("@Proof",dummyT) $ p $ P
+    else P  (*this case discards the proof term*);
+*}
+
+parse_translation {* [("@Proof", proof_tr)] *}
+print_translation {* [("Proof", proof_tr')] *}
+
+axioms
 
 (**** Propositional logic ****)
 
 (*Equality*)
 (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
 
-ieqI      "ideq(a) : a=a"
-ieqE      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
+ieqI:      "ideq(a) : a=a"
+ieqE:      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
 
 (* Truth and Falsity *)
 
-TrueI     "tt : True"
-FalseE    "a:False ==> contr(a):P"
+TrueI:     "tt : True"
+FalseE:    "a:False ==> contr(a):P"
 
 (* Conjunction *)
 
-conjI     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
-conjunct1 "p:P&Q ==> fst(p):P"
-conjunct2 "p:P&Q ==> snd(p):Q"
+conjI:     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
+conjunct1: "p:P&Q ==> fst(p):P"
+conjunct2: "p:P&Q ==> snd(p):Q"
 
 (* Disjunction *)
 
-disjI1    "a:P ==> inl(a):P|Q"
-disjI2    "b:Q ==> inr(b):P|Q"
-disjE     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R 
-          |] ==> when(a,f,g):R"
+disjI1:    "a:P ==> inl(a):P|Q"
+disjI2:    "b:Q ==> inr(b):P|Q"
+disjE:     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R
+           |] ==> when(a,f,g):R"
 
 (* Implication *)
 
-impI      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
-mp        "[| f:P-->Q;  a:P |] ==> f`a:Q"
+impI:      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
+mp:        "[| f:P-->Q;  a:P |] ==> f`a:Q"
 
 (*Quantifiers*)
 
-allI      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
-spec      "(f:ALL x. P(x)) ==> f^x : P(x)"
+allI:      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
+spec:      "(f:ALL x. P(x)) ==> f^x : P(x)"
 
-exI       "p : P(x) ==> [x,p] : EX x. P(x)"
-exE       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
+exI:       "p : P(x) ==> [x,p] : EX x. P(x)"
+exE:       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
 
 (**** Equality between proofs ****)
 
-prefl     "a : P ==> a = a : P"
-psym      "a = b : P ==> b = a : P"
-ptrans    "[| a = b : P;  b = c : P |] ==> a = c : P"
+prefl:     "a : P ==> a = a : P"
+psym:      "a = b : P ==> b = a : P"
+ptrans:    "[| a = b : P;  b = c : P |] ==> a = c : P"
 
-idpeelB   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
+idpeelB:   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
 
-fstB      "a:P ==> fst(<a,b>) = a : P"
-sndB      "b:Q ==> snd(<a,b>) = b : Q"
-pairEC    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
+fstB:      "a:P ==> fst(<a,b>) = a : P"
+sndB:      "b:Q ==> snd(<a,b>) = b : Q"
+pairEC:    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
 
-whenBinl  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
-whenBinr  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
-plusEC    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
+whenBinl:  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
+whenBinr:  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
+plusEC:    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
 
-applyB     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
-funEC      "f:P ==> f = lam x. f`x : P"
+applyB:     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
+funEC:      "f:P ==> f = lam x. f`x : P"
 
-specB      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
+specB:      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
 
 
 (**** Definitions ****)
 
-not_def              "~P == P-->False"
-iff_def         "P<->Q == (P-->Q) & (Q-->P)"
+not_def:              "~P == P-->False"
+iff_def:         "P<->Q == (P-->Q) & (Q-->P)"
 
 (*Unique existence*)
-ex1_def   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+ex1_def:   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
 
 (*Rewriting -- special constants to flag normalized terms and formulae*)
-norm_eq "nrm : norm(x) = x"
-NORM_iff        "NRM : NORM(P) <-> P"
+norm_eq: "nrm : norm(x) = x"
+NORM_iff:        "NRM : NORM(P) <-> P"
+
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
 
-ML
 
-(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
-val show_proofs = ref false;
-
-fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
-
-fun proof_tr' [P,p] = 
-    if !show_proofs then Const("@Proof",dummyT) $ p $ P 
-    else P  (*this case discards the proof term*);
-
-val  parse_translation = [("@Proof", proof_tr)];
-val print_translation  = [("Proof", proof_tr')];
-
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/IsaMakefile
--- a/src/FOLP/IsaMakefile	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/IsaMakefile	Sun Sep 18 14:25:48 2005 +0200
@@ -26,7 +26,7 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/FOLP: $(OUT)/Pure FOLP.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
+$(OUT)/FOLP: $(OUT)/Pure FOLP_lemmas.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
   classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
 
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/ROOT
+(*  Title:      FOLP/ROOT.ML
     ID:         $Id$
     Author:     martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -9,72 +9,6 @@
 *)
 
 val banner = "First-Order Logic with Natural Deduction with Proof Terms";
-
 writeln banner;
 
-print_depth 1;
-
-use_thy "IFOLP";
 use_thy "FOLP";
-
-use "hypsubst.ML";
-use "classical.ML";      (* Patched 'cos matching won't instantiate proof *)
-use "simp.ML";           (* Patched 'cos matching won't instantiate proof *)
-
-
-(*** Applying HypsubstFun to generate hyp_subst_tac ***)
-
-structure Hypsubst_Data =
-  struct
-  (*Take apart an equality judgement; otherwise raise Match!*)
-  fun dest_eq (Const("Proof",_) $ (Const("op =",_)  $ t $ u) $ _) = (t,u);
-
-  val imp_intr = impI
-
-  (*etac rev_cut_eq moves an equality to be the last premise. *)
-  val rev_cut_eq = prove_goal IFOLP.thy 
-                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
-   (fn prems => [ REPEAT(resolve_tac prems 1) ]);
-
-  val rev_mp = rev_mp
-  val subst = subst
-  val sym = sym
-  val thin_refl = prove_goal IFOLP.thy 
-		  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
-  end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
-open Hypsubst;
-
-use "intprover.ML";
-
-(*** Applying ClassicalFun to create a classical prover ***)
-structure Classical_Data = 
-  struct
-  val sizef = size_of_thm
-  val mp = mp
-  val not_elim = notE
-  val swap = swap
-  val hyp_subst_tacs=[hyp_subst_tac]
-  end;
-
-structure Cla = ClassicalFun(Classical_Data);
-open Cla;
-
-(*Propositional rules 
-  -- iffCE might seem better, but in the examples in ex/cla
-     run about 7% slower than with iffE*)
-val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
-                       addSEs [conjE,disjE,impCE,FalseE,iffE];
-
-(*Quantifier rules*)
-val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 
-                      addSEs [exE,ex1E] addEs [allE];
-
-val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I] 
-                          addSEs [exE,ex1E] addEs [all_dupE];
-
-use "simpdata.ML";
-
-
-print_depth 8;
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/If.ML
--- a/src/FOLP/ex/If.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/If.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -1,20 +1,15 @@
-(*  Title:      FOLP/ex/if
+(*  Title:      FOLP/ex/If.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
-
-For ex/if.thy.  First-Order Logic: the 'if' example
 *)
 
-open If;
-open Cla;    (*in case structure Int is open!*)
-
-val prems = goalw If.thy [if_def]
+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 If.thy [if_def]
+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);
@@ -39,5 +34,3 @@
 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();
-
-writeln"Reached end of file.";
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/If.thy
--- a/src/FOLP/ex/If.thy	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/If.thy	Sun Sep 18 14:25:48 2005 +0200
@@ -1,5 +1,13 @@
-If = FOLP +
-consts  if     :: "[o,o,o]=>o"
-rules
-        if_def "if(P,Q,R) == P&Q | ~P&R"
+(* $Id$ *)
+
+theory If
+imports FOLP
+begin
+
+constdefs
+  if :: "[o,o,o]=>o"
+  "if(P,Q,R) == P&Q | ~P&R"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/Nat.ML
--- a/src/FOLP/ex/Nat.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/Nat.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -2,17 +2,8 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
-Examples for the manual "Introduction to Isabelle"
-
-Proofs about the natural numbers
-
-To generate similar output to manual, execute these commands:
-    Pretty.setmargin 72; print_depth 0;
 *)
 
-open Nat;
-
 Goal "?p : ~ (Suc(k) = k)";
 by (res_inst_tac [("n","k")] induct 1);
 by (rtac notI 1);
@@ -42,23 +33,23 @@
 val add_Suc = result();
 
 (*
-val nat_congs = mk_congs Nat.thy ["Suc", "op +"];
+val nat_congs = mk_congs (the_context ()) ["Suc", "op +"];
 prths nat_congs;
 *)
-val prems = goal Nat.thy "p: x=y ==> ?p : Suc(x) = Suc(y)";
+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 Nat.thy "[| 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 
+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  
+val add_ss = FOLP_ss  addcongs nat_congs
                      addrews  [add_0, add_Suc];
 
 Goal "?p : (k+m)+n = k+(m+n)";
@@ -79,4 +70,3 @@
 val add_Suc_right = result();
 
 (*mk_typed_congs appears not to work with FOLP's version of subst*)
-
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/Nat.thy	Sun Sep 18 14:25:48 2005 +0200
@@ -2,15 +2,16 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
-Examples for the manual "Introduction to Isabelle"
-
-Theory of the natural numbers: Peano's axioms, primitive recursion
 *)
 
-Nat = IFOLP +
-types   nat
-arities nat         :: term
+header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
+
+theory Nat
+imports FOLP
+begin
+
+typedecl nat
+arities nat         :: "term"
 consts  "0"         :: "nat"    ("0")
         Suc         :: "nat=>nat"
         rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
@@ -18,19 +19,24 @@
 
   (*Proof terms*)
        nrec         :: "[nat,p,[nat,p]=>p]=>p"
-       ninj,nneq    :: "p=>p"
-       rec0, recSuc :: "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))
+              |] ==> nrec(n,b,c):P(n)"
 
-rules   
-  induct     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x)) 
-             |] ==> nrec(n,b,c):P(n)"
-  
-  Suc_inject "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
-  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))"
-  add_def    "m+n == rec(m, n, %x y. Suc(y))"
+  Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
+  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))"
+  add_def:    "m+n == rec(m, n, %x y. Suc(y))"
 
-  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"
+  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 ()) *}
+
 end
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/ROOT.ML
--- a/src/FOLP/ex/ROOT.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -1,9 +1,9 @@
-(*  Title:      FOLP/ex/ROOT
+(*  Title:      FOLP/ex/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Executes all examples for First-Order Logic. 
+Examples for First-Order Logic. 
 *)
 
 time_use     "intro.ML";
@@ -13,7 +13,7 @@
 writeln"\n** Intuitionistic examples **\n";
 time_use     "int.ML";
 
-val thy = IFOLP.thy  and  tac = IntPr.fast_tac 1;
+val thy = theory "IFOLP"  and  tac = IntPr.fast_tac 1;
 time_use     "prop.ML";
 time_use     "quant.ML";
 
@@ -21,6 +21,6 @@
 time_use     "cla.ML";
 time_use_thy "If";
 
-val thy = FOLP.thy  and  tac = Cla.fast_tac FOLP_cs 1;
+val thy = theory "FOLP"  and  tac = Cla.fast_tac FOLP_cs 1;
 time_use     "prop.ML";
 time_use     "quant.ML";
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/cla.ML
--- a/src/FOLP/ex/cla.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/cla.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -3,24 +3,20 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Classical First-Order Logic
+Classical First-Order Logic.
 *)
 
-writeln"File FOLP/ex/cla.ML";
-
-open Cla;    (*in case structure Int is open!*)
-
-goal FOLP.thy "?p : (P --> Q | R) --> (P-->Q) | (P-->R)";
+goal (theory "FOLP") "?p : (P --> Q | R) --> (P-->Q) | (P-->R)";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*If and only if*)
 
-goal FOLP.thy "?p : (P<->Q) <-> (Q<->P)";
+goal (theory "FOLP") "?p : (P<->Q) <-> (Q<->P)";
 by (fast_tac FOLP_cs 1);
 result();
 
-goal FOLP.thy "?p : ~ (P <-> ~P)";
+goal (theory "FOLP") "?p : ~ (P <-> ~P)";
 by (fast_tac FOLP_cs 1);
 result();
 
@@ -37,105 +33,105 @@
 
 writeln"Pelletier's examples";
 (*1*)
-goal FOLP.thy "?p : (P-->Q)  <->  (~Q --> ~P)";
+goal (theory "FOLP") "?p : (P-->Q)  <->  (~Q --> ~P)";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*2*)
-goal FOLP.thy "?p : ~ ~ P  <->  P";
+goal (theory "FOLP") "?p : ~ ~ P  <->  P";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*3*)
-goal FOLP.thy "?p : ~(P-->Q) --> (Q-->P)";
+goal (theory "FOLP") "?p : ~(P-->Q) --> (Q-->P)";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*4*)
-goal FOLP.thy "?p : (~P-->Q)  <->  (~Q --> P)";
+goal (theory "FOLP") "?p : (~P-->Q)  <->  (~Q --> P)";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*5*)
-goal FOLP.thy "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))";
+goal (theory "FOLP") "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*6*)
-goal FOLP.thy "?p : P | ~ P";
+goal (theory "FOLP") "?p : P | ~ P";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*7*)
-goal FOLP.thy "?p : P | ~ ~ ~ P";
+goal (theory "FOLP") "?p : P | ~ ~ ~ P";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*8.  Peirce's law*)
-goal FOLP.thy "?p : ((P-->Q) --> P)  -->  P";
+goal (theory "FOLP") "?p : ((P-->Q) --> P)  -->  P";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*9*)
-goal FOLP.thy "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
+goal (theory "FOLP") "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*10*)
-goal FOLP.thy "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)";
+goal (theory "FOLP") "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
-goal FOLP.thy "?p : P<->P";
+goal (theory "FOLP") "?p : P<->P";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*12.  "Dijkstra's law"*)
-goal FOLP.thy "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
+goal (theory "FOLP") "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*13.  Distributive law*)
-goal FOLP.thy "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
+goal (theory "FOLP") "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*14*)
-goal FOLP.thy "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
+goal (theory "FOLP") "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*15*)
-goal FOLP.thy "?p : (P --> Q) <-> (~P | Q)";
+goal (theory "FOLP") "?p : (P --> Q) <-> (~P | Q)";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*16*)
-goal FOLP.thy "?p : (P-->Q) | (Q-->P)";
+goal (theory "FOLP") "?p : (P-->Q) | (Q-->P)";
 by (fast_tac FOLP_cs 1);
 result();
 
 (*17*)
-goal FOLP.thy "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
+goal (theory "FOLP") "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
 by (fast_tac FOLP_cs 1);
 result();
 
 writeln"Classical Logic: examples with quantifiers";
 
-goal FOLP.thy "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
+goal (theory "FOLP") "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
 by (fast_tac FOLP_cs 1);
 result(); 
 
-goal FOLP.thy "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
+goal (theory "FOLP") "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
 by (fast_tac FOLP_cs 1);
 result(); 
 
-goal FOLP.thy "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
+goal (theory "FOLP") "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
 by (fast_tac FOLP_cs 1);
 result(); 
 
-goal FOLP.thy "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
+goal (theory "FOLP") "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
 by (fast_tac FOLP_cs 1);
 result(); 
 
@@ -143,16 +139,16 @@
 
 (*Needs multiple instantiation of ALL.*)
 (*
-goal FOLP.thy "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
+goal (theory "FOLP") "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
 by (best_tac FOLP_dup_cs 1);
 result();
 *)
 (*Needs double instantiation of the quantifier*)
-goal FOLP.thy "?p : EX x. P(x) --> P(a) & P(b)";
+goal (theory "FOLP") "?p : EX x. P(x) --> P(a) & P(b)";
 by (best_tac FOLP_dup_cs 1);
 result();
 
-goal FOLP.thy "?p : EX z. P(z) --> (ALL x. P(x))";
+goal (theory "FOLP") "?p : EX z. P(z) --> (ALL x. P(x))";
 by (best_tac FOLP_dup_cs 1);
 result();
 
@@ -160,45 +156,45 @@
 writeln"Hard examples with quantifiers";
 
 writeln"Problem 18";
-goal FOLP.thy "?p : EX y. ALL x. P(y)-->P(x)";
+goal (theory "FOLP") "?p : EX y. ALL x. P(y)-->P(x)";
 by (best_tac FOLP_dup_cs 1);
 result(); 
 
 writeln"Problem 19";
-goal FOLP.thy "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
+goal (theory "FOLP") "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
 by (best_tac FOLP_dup_cs 1);
 result();
 
 writeln"Problem 20";
-goal FOLP.thy "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
+goal (theory "FOLP") "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
 \   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
 by (fast_tac FOLP_cs 1); 
 result();
 (*
 writeln"Problem 21";
-goal FOLP.thy "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
+goal (theory "FOLP") "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
 by (best_tac FOLP_dup_cs 1);
 result();
 *)
 writeln"Problem 22";
-goal FOLP.thy "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
+goal (theory "FOLP") "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
 by (fast_tac FOLP_cs 1); 
 result();
 
 writeln"Problem 23";
-goal FOLP.thy "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
+goal (theory "FOLP") "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
 by (best_tac FOLP_cs 1);  
 result();
 
 writeln"Problem 24";
-goal FOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
+goal (theory "FOLP") "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
 \    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
 \   --> (EX x. P(x)&R(x))";
 by (fast_tac FOLP_cs 1); 
 result();
 (*
 writeln"Problem 25";
-goal FOLP.thy "?p : (EX x. P(x)) &  \
+goal (theory "FOLP") "?p : (EX x. P(x)) &  \
 \       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
 \       (ALL x. P(x) --> (M(x) & L(x))) &   \
 \       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
@@ -207,14 +203,14 @@
 result();
 
 writeln"Problem 26";
-goal FOLP.thy "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   \
+goal (theory "FOLP") "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   \
 \     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
 \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
 by (fast_tac FOLP_cs 1);
 result();
 *)
 writeln"Problem 27";
-goal FOLP.thy "?p : (EX x. P(x) & ~Q(x)) &   \
+goal (theory "FOLP") "?p : (EX x. P(x) & ~Q(x)) &   \
 \             (ALL x. P(x) --> R(x)) &   \
 \             (ALL x. M(x) & L(x) --> P(x)) &   \
 \             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
@@ -223,7 +219,7 @@
 result();
 
 writeln"Problem 28.  AMENDED";
-goal FOLP.thy "?p : (ALL x. P(x) --> (ALL x. Q(x))) &   \
+goal (theory "FOLP") "?p : (ALL x. P(x) --> (ALL x. Q(x))) &   \
 \       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
 \       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
 \   --> (ALL x. P(x) & L(x) --> M(x))";
@@ -231,21 +227,21 @@
 result();
 
 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
-goal FOLP.thy "?p : (EX x. P(x)) & (EX y. Q(y))  \
+goal (theory "FOLP") "?p : (EX x. P(x)) & (EX y. Q(y))  \
 \   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
 \        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
 by (fast_tac FOLP_cs 1); 
 result();
 
 writeln"Problem 30";
-goal FOLP.thy "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) & \
+goal (theory "FOLP") "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) & \
 \       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
 \   --> (ALL x. S(x))";
 by (fast_tac FOLP_cs 1);  
 result();
 
 writeln"Problem 31";
-goal FOLP.thy "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
+goal (theory "FOLP") "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
 \       (EX x. L(x) & P(x)) & \
 \       (ALL x. ~ R(x) --> M(x))  \
 \   --> (EX x. L(x) & M(x))";
@@ -253,7 +249,7 @@
 result();
 
 writeln"Problem 32";
-goal FOLP.thy "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
+goal (theory "FOLP") "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
 \       (ALL x. S(x) & R(x) --> L(x)) & \
 \       (ALL x. M(x) --> R(x))  \
 \   --> (ALL x. P(x) & M(x) --> L(x))";
@@ -261,18 +257,18 @@
 result();
 
 writeln"Problem 33";
-goal FOLP.thy "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
+goal (theory "FOLP") "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
 \    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
 by (best_tac FOLP_cs 1);
 result();
 
 writeln"Problem 35";
-goal FOLP.thy "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))";
+goal (theory "FOLP") "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))";
 by (best_tac FOLP_dup_cs 1);
 result();
 
 writeln"Problem 36";
-goal FOLP.thy
+goal (theory "FOLP")
 "?p : (ALL x. EX y. J(x,y)) & \
 \     (ALL x. EX y. G(x,y)) & \
 \     (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
@@ -281,7 +277,7 @@
 result();
 
 writeln"Problem 37";
-goal FOLP.thy "?p : (ALL z. EX w. ALL x. EX y. \
+goal (theory "FOLP") "?p : (ALL z. EX w. ALL x. EX y. \
 \          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
 \       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
 \       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
@@ -290,24 +286,24 @@
 result();
 
 writeln"Problem 39";
-goal FOLP.thy "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
+goal (theory "FOLP") "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
 by (fast_tac FOLP_cs 1);
 result();
 
 writeln"Problem 40.  AMENDED";
-goal FOLP.thy "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
+goal (theory "FOLP") "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
 \             ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
 by (fast_tac FOLP_cs 1);
 result();
 
 writeln"Problem 41";
-goal FOLP.thy "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))  \
+goal (theory "FOLP") "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))  \
 \         --> ~ (EX z. ALL x. f(x,z))";
 by (best_tac FOLP_cs 1);
 result();
 
 writeln"Problem 44";
-goal FOLP.thy "?p : (ALL x. f(x) -->                                    \
+goal (theory "FOLP") "?p : (ALL x. f(x) -->                                    \
 \             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
 \             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
 \             --> (EX x. j(x) & ~f(x))";
@@ -317,44 +313,42 @@
 writeln"Problems (mainly) involving equality or functions";
 
 writeln"Problem 48";
-goal FOLP.thy "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
+goal (theory "FOLP") "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
 by (fast_tac FOLP_cs 1);
 result();
 
 writeln"Problem 50";  
 (*What has this to do with equality?*)
-goal FOLP.thy "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
+goal (theory "FOLP") "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
 by (best_tac FOLP_dup_cs 1);
 result();
 
 writeln"Problem 56";
-goal FOLP.thy
+goal (theory "FOLP")
  "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
 by (fast_tac FOLP_cs 1);
 result();
 
 writeln"Problem 57";
-goal FOLP.thy
+goal (theory "FOLP")
 "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
 \     (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
 by (fast_tac FOLP_cs 1);
 result();
 
 writeln"Problem 58  NOT PROVED AUTOMATICALLY";
-goal FOLP.thy "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
+goal (theory "FOLP") "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
 val f_cong = read_instantiate [("t","f")] subst_context;
 by (fast_tac (FOLP_cs addIs [f_cong]) 1);
 result();
 
 writeln"Problem 59";
-goal FOLP.thy "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
+goal (theory "FOLP") "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
 by (best_tac FOLP_dup_cs 1);
 result();
 
 writeln"Problem 60";
-goal FOLP.thy
+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();
-
-writeln"Reached end of file.";
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/foundn.ML
--- a/src/FOLP/ex/foundn.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/foundn.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -6,9 +6,7 @@
 Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
 *)
 
-writeln"File FOLP/ex/foundn.ML";
-
-goal IFOLP.thy "?p : A&B  --> (C-->A&C)";
+goal (theory "IFOLP") "?p : A&B  --> (C-->A&C)";
 by (rtac impI 1);
 by (rtac impI 1);
 by (rtac conjI 1);
@@ -19,7 +17,7 @@
 
 (*A form of conj-elimination*)
 val prems = 
-goal IFOLP.thy "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
+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);
@@ -29,7 +27,7 @@
 
 
 val prems = 
-goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
+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);
@@ -47,7 +45,7 @@
 
 
 val prems = 
-goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
+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);
@@ -61,7 +59,7 @@
 
 
 val prems = 
-goal IFOLP.thy "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
+goal (theory "IFOLP") "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
 by (rtac disjE 1);
 by (resolve_tac prems 1);
 by (assume_tac 1);
@@ -75,7 +73,7 @@
 writeln"Examples with quantifiers";
 
 val prems =
-goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
+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); 
@@ -84,14 +82,14 @@
 result();
 
 
-goal IFOLP.thy "?p : ALL x. EX y. x=y";
+goal (theory "IFOLP") "?p : ALL x. EX y. x=y";
 by (rtac allI 1);
 by (rtac exI 1);
 by (rtac refl 1);
 result();
 
 
-goal IFOLP.thy "?p : EX y. ALL x. x=y";
+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";  
@@ -99,7 +97,7 @@
 
 
 (*Parallel lifting example. *)
-goal IFOLP.thy "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
+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);
@@ -108,7 +106,7 @@
 
 
 val prems =
-goal IFOLP.thy "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
+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);
@@ -121,7 +119,7 @@
 
 
 (*A bigger demonstration of quantifiers -- not in the paper*)
-goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
+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);
@@ -129,6 +127,3 @@
 by (rtac allE 1 THEN assume_tac 1);
 by (assume_tac 1);
 result();  
-
-
-writeln"Reached end of file.";
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/int.ML
--- a/src/FOLP/ex/int.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/int.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -15,8 +15,6 @@
 by (IntPr.fast_tac 1);
 *)
 
-writeln"File FOLP/ex/int.ML";
-
 (*Note: for PROPOSITIONAL formulae...
   ~A is classically provable iff it is intuitionistically provable.  
   Therefore A is classically provable iff ~~A is intuitionistically provable.
@@ -29,34 +27,34 @@
 ~~P is intuitionstically equivalent to P.  [Andy Pitts]
 *)
 
-goal IFOLP.thy "?p : ~~(P&Q) <-> ~~P & ~~Q";
+goal (theory "IFOLP") "?p : ~~(P&Q) <-> ~~P & ~~Q";
 by (IntPr.fast_tac 1);
 result();
 
-goal IFOLP.thy "?p : ~~~P <-> ~P";
+goal (theory "IFOLP") "?p : ~~~P <-> ~P";
 by (IntPr.fast_tac 1);
 result();
 
-goal IFOLP.thy "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))";
+goal (theory "IFOLP") "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))";
 by (IntPr.fast_tac 1);
 result();
 
-goal IFOLP.thy "?p : (P<->Q) <-> (Q<->P)";
+goal (theory "IFOLP") "?p : (P<->Q) <-> (Q<->P)";
 by (IntPr.fast_tac 1);
 result();
 
 
 writeln"Lemmas for the propositional double-negation translation";
 
-goal IFOLP.thy "?p : P --> ~~P";
+goal (theory "IFOLP") "?p : P --> ~~P";
 by (IntPr.fast_tac 1);
 result();
 
-goal IFOLP.thy "?p : ~~(~~P --> P)";
+goal (theory "IFOLP") "?p : ~~(~~P --> P)";
 by (IntPr.fast_tac 1);
 result();
 
-goal IFOLP.thy "?p : ~~P & ~~(P --> Q) --> ~~Q";
+goal (theory "IFOLP") "?p : ~~P & ~~(P --> Q) --> ~~Q";
 by (IntPr.fast_tac 1);
 result();
 
@@ -64,12 +62,12 @@
 writeln"The following are classically but not constructively valid.";
 
 (*The attempt to prove them terminates quickly!*)
-goal IFOLP.thy "?p : ((P-->Q) --> P)  -->  P";
+goal (theory "IFOLP") "?p : ((P-->Q) --> P)  -->  P";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 (*Check that subgoals remain: proof failed.*)
 getgoal 1;  
 
-goal IFOLP.thy "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)";
+goal (theory "IFOLP") "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1;  
 
@@ -77,99 +75,99 @@
 writeln"Intuitionistic FOL: propositional problems based on Pelletier.";
 
 writeln"Problem ~~1";
-goal IFOLP.thy "?p : ~~((P-->Q)  <->  (~Q --> ~P))";
+goal (theory "IFOLP") "?p : ~~((P-->Q)  <->  (~Q --> ~P))";
 by (IntPr.fast_tac 1);
 result();
 (*5 secs*)
 
 
 writeln"Problem ~~2";
-goal IFOLP.thy "?p : ~~(~~P  <->  P)";
+goal (theory "IFOLP") "?p : ~~(~~P  <->  P)";
 by (IntPr.fast_tac 1);
 result();
 (*1 secs*)
 
 
 writeln"Problem 3";
-goal IFOLP.thy "?p : ~(P-->Q) --> (Q-->P)";
+goal (theory "IFOLP") "?p : ~(P-->Q) --> (Q-->P)";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem ~~4";
-goal IFOLP.thy "?p : ~~((~P-->Q)  <->  (~Q --> P))";
+goal (theory "IFOLP") "?p : ~~((~P-->Q)  <->  (~Q --> P))";
 by (IntPr.fast_tac 1);
 result();
 (*9 secs*)
 
 writeln"Problem ~~5";
-goal IFOLP.thy "?p : ~~((P|Q-->P|R) --> P|(Q-->R))";
+goal (theory "IFOLP") "?p : ~~((P|Q-->P|R) --> P|(Q-->R))";
 by (IntPr.fast_tac 1);
 result();
 (*10 secs*)
 
 
 writeln"Problem ~~6";
-goal IFOLP.thy "?p : ~~(P | ~P)";
+goal (theory "IFOLP") "?p : ~~(P | ~P)";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem ~~7";
-goal IFOLP.thy "?p : ~~(P | ~~~P)";
+goal (theory "IFOLP") "?p : ~~(P | ~~~P)";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem ~~8.  Peirce's law";
-goal IFOLP.thy "?p : ~~(((P-->Q) --> P)  -->  P)";
+goal (theory "IFOLP") "?p : ~~(((P-->Q) --> P)  -->  P)";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem 9";
-goal IFOLP.thy "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
+goal (theory "IFOLP") "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
 by (IntPr.fast_tac 1);
 result();
 (*9 secs*)
 
 
 writeln"Problem 10";
-goal IFOLP.thy "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)";
+goal (theory "IFOLP") "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"11.  Proved in each direction (incorrectly, says Pelletier!!) ";
-goal IFOLP.thy "?p : P<->P";
+goal (theory "IFOLP") "?p : P<->P";
 by (IntPr.fast_tac 1);
 
 writeln"Problem ~~12.  Dijkstra's law  ";
-goal IFOLP.thy "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))";
+goal (theory "IFOLP") "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))";
 by (IntPr.fast_tac 1);
 result();
 
-goal IFOLP.thy "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))";
+goal (theory "IFOLP") "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem 13.  Distributive law";
-goal IFOLP.thy "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
+goal (theory "IFOLP") "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem ~~14";
-goal IFOLP.thy "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))";
+goal (theory "IFOLP") "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem ~~15";
-goal IFOLP.thy "?p : ~~((P --> Q) <-> (~P | Q))";
+goal (theory "IFOLP") "?p : ~~((P --> Q) <-> (~P | Q))";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem ~~16";
-goal IFOLP.thy "?p : ~~((P-->Q) | (Q-->P))";
+goal (theory "IFOLP") "?p : ~~((P-->Q) | (Q-->P))";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem ~~17";
-goal IFOLP.thy
+goal (theory "IFOLP")
   "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))";
 by (IntPr.fast_tac 1);
 (*over 5 minutes?? -- printing the proof term takes 40 secs!!*)
@@ -180,23 +178,23 @@
 
 writeln"The converse is classical in the following implications...";
 
-goal IFOLP.thy "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q";
+goal (theory "IFOLP") "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q";
 by (IntPr.fast_tac 1); 
 result();  
 
-goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
+goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
 by (IntPr.fast_tac 1); 
 result();  
 
-goal IFOLP.thy "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))";
+goal (theory "IFOLP") "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))";
 by (IntPr.fast_tac 1); 
 result();  
 
-goal IFOLP.thy "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)";
+goal (theory "IFOLP") "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)";
 by (IntPr.fast_tac 1); 
 result();  
 
-goal IFOLP.thy "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))";
+goal (theory "IFOLP") "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))";
 by (IntPr.fast_tac 1);
 result();  
 
@@ -206,24 +204,24 @@
 writeln"The following are not constructively valid!";
 (*The attempt to prove them terminates quickly!*)
 
-goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
+goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
-goal IFOLP.thy "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
+goal (theory "IFOLP") "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
-goal IFOLP.thy "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
+goal (theory "IFOLP") "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
-goal IFOLP.thy "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
+goal (theory "IFOLP") "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
 (*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
-goal IFOLP.thy "?p : EX x. Q(x) --> (ALL x. Q(x))";
+goal (theory "IFOLP") "?p : EX x. Q(x) --> (ALL x. Q(x))";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
@@ -234,36 +232,36 @@
   Some will require quantifier duplication -- not currently available*)
 
 writeln"Problem ~~18";
-goal IFOLP.thy "?p : ~~(EX y. ALL x. P(y)-->P(x))";
+goal (theory "IFOLP") "?p : ~~(EX y. ALL x. P(y)-->P(x))";
 (*NOT PROVED*)
 
 writeln"Problem ~~19";
-goal IFOLP.thy "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))";
+goal (theory "IFOLP") "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))";
 (*NOT PROVED*)
 
 writeln"Problem 20";
-goal IFOLP.thy "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
+goal (theory "IFOLP") "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
 \   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
 by (IntPr.fast_tac 1); 
 result();
 
 writeln"Problem 21";
-goal IFOLP.thy
+goal (theory "IFOLP")
     "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))";
 (*NOT PROVED*)
 
 writeln"Problem 22";
-goal IFOLP.thy "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
+goal (theory "IFOLP") "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
 by (IntPr.fast_tac 1); 
 result();
 
 writeln"Problem ~~23";
-goal IFOLP.thy "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))";
+goal (theory "IFOLP") "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))";
 by (IntPr.best_tac 1);  
 result();
 
 writeln"Problem 24";
-goal IFOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
+goal (theory "IFOLP") "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
 \    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
 \   --> ~~(EX x. P(x)&R(x))";
 (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
@@ -274,7 +272,7 @@
 result();
 
 writeln"Problem 25";
-goal IFOLP.thy "?p : (EX x. P(x)) &  \
+goal (theory "IFOLP") "?p : (EX x. P(x)) &  \
 \       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
 \       (ALL x. P(x) --> (M(x) & L(x))) &   \
 \       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
@@ -283,21 +281,21 @@
 result();
 
 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
-goal IFOLP.thy "?p : (EX x. P(x)) & (EX y. Q(y))  \
+goal (theory "IFOLP") "?p : (EX x. P(x)) & (EX y. Q(y))  \
 \   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
 \        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
 by (IntPr.fast_tac 1); 
 result();
 
 writeln"Problem ~~30";
-goal IFOLP.thy "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & \
+goal (theory "IFOLP") "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & \
 \       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
 \   --> (ALL x. ~~S(x))";
 by (IntPr.fast_tac 1);  
 result();
 
 writeln"Problem 31";
-goal IFOLP.thy "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
+goal (theory "IFOLP") "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
 \       (EX x. L(x) & P(x)) & \
 \       (ALL x. ~ R(x) --> M(x))  \
 \   --> (EX x. L(x) & M(x))";
@@ -305,7 +303,7 @@
 result();
 
 writeln"Problem 32";
-goal IFOLP.thy "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
+goal (theory "IFOLP") "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
 \       (ALL x. S(x) & R(x) --> L(x)) & \
 \       (ALL x. M(x) --> R(x))  \
 \   --> (ALL x. P(x) & M(x) --> L(x))";
@@ -313,18 +311,18 @@
 result();
 
 writeln"Problem 39";
-goal IFOLP.thy "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
+goal (theory "IFOLP") "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem 40.  AMENDED";
-goal IFOLP.thy "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
+goal (theory "IFOLP") "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
 \             ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem 44";
-goal IFOLP.thy "?p : (ALL x. f(x) -->                                   \
+goal (theory "IFOLP") "?p : (ALL x. f(x) -->                                   \
 \             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
 \             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
 \             --> (EX x. j(x) & ~f(x))";
@@ -332,34 +330,32 @@
 result();
 
 writeln"Problem 48";
-goal IFOLP.thy "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
+goal (theory "IFOLP") "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem 51";
-goal IFOLP.thy
+goal (theory "IFOLP")
     "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
 \    (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
 by (IntPr.best_tac 1);  (*60 seconds*)
 result();
 
 writeln"Problem 56";
-goal IFOLP.thy
+goal (theory "IFOLP")
     "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem 57";
-goal IFOLP.thy
+goal (theory "IFOLP")
     "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
 \    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
 by (IntPr.fast_tac 1);
 result();
 
 writeln"Problem 60";
-goal IFOLP.thy
+goal (theory "IFOLP")
     "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
 by (IntPr.fast_tac 1);
 result();
-
-writeln"Reached end of file.";
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/intro.ML
--- a/src/FOLP/ex/intro.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/intro.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -14,7 +14,7 @@
 
 (**** Some simple backward proofs ****)
 
-goal FOLP.thy "?p:P|P --> P";
+goal (theory "FOLP") "?p:P|P --> P";
 by (rtac impI 1);
 by (rtac disjE 1);
 by (assume_tac 3);
@@ -22,7 +22,7 @@
 by (assume_tac 1);
 val mythm = result();
 
-goal FOLP.thy "?p:(P & Q) | R  --> (P | R)";
+goal (theory "FOLP") "?p:(P & Q) | R  --> (P | R)";
 by (rtac impI 1);
 by (etac disjE 1);
 by (dtac conjunct1 1);
@@ -32,7 +32,7 @@
 result();
 
 (*Correct version, delaying use of "spec" until last*)
-goal FOLP.thy "?p:(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
+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);
@@ -44,12 +44,12 @@
 
 (**** Demonstration of fast_tac ****)
 
-goal FOLP.thy "?p:(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
+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 FOLP.thy "?p:ALL x. P(x,f(x)) <-> \
+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();
@@ -57,7 +57,7 @@
 
 (**** Derivation of conjunction elimination rule ****)
 
-val [major,minor] = goal FOLP.thy "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
+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);
@@ -69,14 +69,14 @@
 
 (** Derivation of negation introduction **)
 
-val prems = goal FOLP.thy "(!!x. x:P ==> f(x):False) ==> ?p:~P";
+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 FOLP.thy "[| p:~P;  q:P |] ==> ?p:R";
+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);
@@ -84,9 +84,7 @@
 result();
 
 (*Alternative proof of above result*)
-val [major,minor] = goalw FOLP.thy [not_def]
+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();
-
-writeln"Reached end of file.";
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/prop.ML
--- a/src/FOLP/ex/prop.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/prop.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -7,9 +7,6 @@
 Needs declarations of the theory "thy" and the tactic "tac"
 *)
 
-writeln"File FOLP/ex/prop.ML";
-
-
 writeln"commutative laws of & and | ";
 Goal "?p : P & Q  -->  Q & P";
 by tac;
@@ -149,5 +146,3 @@
 \    --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5";
 by tac;
 result();
-
-writeln"Reached end of file.";
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/ex/quant.ML
--- a/src/FOLP/ex/quant.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/quant.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -7,101 +7,99 @@
 Needs declarations of the theory "thy" and the tactic "tac"
 *)
 
-writeln"File FOLP/ex/quant.ML";
-
 Goal "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
 by tac;
-result();  
+result();
 
 
 Goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
 by tac;
-result();  
+result();
 
 
 (*Converse is false*)
 Goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
 by tac;
-result();  
+result();
 
 Goal "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
 by tac;
-result();  
+result();
 
 
 Goal "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
 by tac;
-result();  
+result();
 
 
 writeln"Some harder ones";
 
 Goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
 by tac;
-result();  
+result();
 (*6 secs*)
 
 (*Converse is false*)
 Goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))";
 by tac;
-result();  
+result();
 
 
 writeln"Basic test of quantifier reasoning";
 (*TRUE*)
 Goal "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
-by tac;  
-result();  
+by tac;
+result();
 
 
 Goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))";
-by tac;  
-result();  
+by tac;
+result();
 
 
 writeln"The following should fail, as they are false!";
 
 Goal "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
-by tac handle ERROR => writeln"Failed, as expected";  
+by tac handle ERROR => writeln"Failed, as expected";
 (*Check that subgoals remain: proof failed.*)
-getgoal 1; 
+getgoal 1;
 
 Goal "?p : (EX x. Q(x))  -->  (ALL x. Q(x))";
-by tac handle ERROR => writeln"Failed, as expected";  
-getgoal 1; 
+by tac handle ERROR => writeln"Failed, as expected";
+getgoal 1;
 
 Goal "?p : P(?a) --> (ALL x. P(x))";
 by tac handle ERROR => writeln"Failed, as expected";
 (*Check that subgoals remain: proof failed.*)
-getgoal 1;  
+getgoal 1;
 
 Goal
     "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
 by tac handle ERROR => writeln"Failed, as expected";
-getgoal 1;  
+getgoal 1;
 
 
 writeln"Back to things that are provable...";
 
 Goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
-by tac;  
-result();  
+by tac;
+result();
 
 
 (*An example of why exI should be delayed as long as possible*)
 Goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
-by tac;  
-result();  
+by tac;
+result();
 
 Goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
-by tac; 
-(*Verify that no subgoals remain.*) 
-uresult();  
+by tac;
+(*Verify that no subgoals remain.*)
+uresult();
 
 
 Goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))";
 by tac;
-result();  
+result();
 
 
 writeln"Some slow ones";
@@ -110,20 +108,17 @@
 (*Principia Mathematica *11.53  *)
 Goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
 by tac;
-result();  
+result();
 (*6 secs*)
 
 (*Principia Mathematica *11.55  *)
 Goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
 by tac;
-result();  
+result();
 (*9 secs*)
 
 (*Principia Mathematica *11.61  *)
 Goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
 by tac;
-result();  
+result();
 (*3 secs*)
-
-writeln"Reached end of file.";
-
diff -r 68a7acb5f22e -r fd19f77dcf60 src/FOLP/simpdata.ML
--- a/src/FOLP/simpdata.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/simpdata.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -3,13 +3,13 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Simplification data for FOLP
+Simplification data for FOLP.
 *)
 
 (*** Rewrite rules ***)
 
-fun int_prove_fun_raw s = 
-    (writeln s;  prove_goal IFOLP.thy s
+fun int_prove_fun_raw s =
+    (writeln s;  prove_goal (the_context ()) s
        (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
 
 fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
@@ -32,7 +32,7 @@
 
 val imp_rews = map int_prove_fun
  ["(P --> False) <-> ~P",       "(P --> True) <-> True",
-  "(False --> P) <-> True",     "(True --> P) <-> P", 
+  "(False --> P) <-> True",     "(True --> P) <-> P",
   "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
 
 val iff_rews = map int_prove_fun
@@ -70,7 +70,7 @@
 fun mk_eq th = case concl_of th of
       _ $ (Const("op <->",_)$_$_) $ _ => th
     | _ $ (Const("op =",_)$_$_) $ _ => th
-    | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F 
+    | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F
     | _ => make_iff_T th;
 
 
@@ -113,12 +113,12 @@
 structure FOLP_Simp = SimpFun(FOLP_SimpData);
 
 (*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
-val FOLP_congs = 
+val FOLP_congs =
    [all_cong,ex_cong,eq_cong,
     conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
 
 val IFOLP_rews =
-   [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
+   [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
     imp_rews @ iff_rews @ quant_rews;
 
 open FOLP_Simp;
@@ -128,8 +128,8 @@
 val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
 
 (*Classical version...*)
-fun prove_fun s = 
-    (writeln s;  prove_goal FOLP.thy s
+fun prove_fun s =
+    (writeln s;  prove_goal (the_context ()) s
        (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
 
 val cla_rews = map prove_fun
@@ -139,5 +139,3 @@
 val FOLP_rews = IFOLP_rews@cla_rews;
 
 val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;
-
-