# HG changeset patch
# User wenzelm
# Date 1127049608 -7200
# Node ID 75166ebb619b8ad17553a7351cf6583f41a9caac
# Parent  fd19f77dcf6003bafc64c130d7b8bfee825ff687
converted to Isar theory format;

diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/ILL.ML
--- a/src/Sequents/ILL.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -2,19 +2,18 @@
     ID:         $Id$
     Author:     Sara Kalvala and Valeria de Paiva
     Copyright   1992  University of Cambridge
-
 *)
 
 val lazy_cs = empty_pack
  add_safes [tensl, conjr, disjl, promote0,
-	    context2,context3]
+            context2,context3]
  add_unsafes [identity, zerol, conjll, conjlr, disjrl, disjrr,
-	       impr, tensr, impl, derelict, weaken,
-		 promote1, promote2,context1,context4a,context4b];
+               impr, tensr, impl, derelict, weaken,
+                 promote1, promote2,context1,context4a,context4b];
 
 fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n);
 
-fun auto x = prove_goal thy x (fn prems => [best_tac lazy_cs 1]);
+fun auto x = prove_goal (the_context ()) x (fn prems => [best_tac lazy_cs 1]);
 
 Goal "$F, $G |- A ==> $F, !(A -o B), $G |- B";
 by (rtac derelict 1);
@@ -52,7 +51,7 @@
 by (assume_tac 1);
 qed "impr_contr_der";
 
-val _ = goal thy "$F, (!B) -o 0, $G, !B, $H |- A";
+val _ = goal (the_context ()) "$F, (!B) -o 0, $G, !B, $H |- A";
 by (rtac impl 1);
 by (rtac identity 3);
 by (rtac context3 1);
@@ -61,7 +60,7 @@
 qed "contrad1";
 
 
-val _ = goal thy "$F, !B, $G, (!B) -o 0, $H |- A";
+val _ = goal (the_context ()) "$F, !B, $G, (!B) -o 0, $H |- A";
 by (rtac impl 1);
 by (rtac identity 3);
 by (rtac context3 1);
@@ -69,7 +68,7 @@
 by (rtac zerol 1);
 qed "contrad2";
 
-val _ = goal thy "A -o B, A |- B";
+val _ = goal (the_context ()) "A -o B, A |- B";
 by (rtac impl 1);
 by (rtac identity 2);
 by (rtac identity 2);
@@ -94,7 +93,7 @@
 by (rtac context1 1);
 qed "mp_rule2";
 
-val _ = goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
+val _ = goal (the_context ()) "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
 by (best_tac lazy_cs 1);
 qed "or_to_and";
 
@@ -109,7 +108,7 @@
 
 
 
-val _ = goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
+val _ = goal (the_context ()) "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
 by (rtac impr 1);
 by (rtac conj_lemma 1);
 by (rtac disjl 1);
@@ -136,20 +135,20 @@
 qed "a_not_a_rule";
 
 fun thm_to_rule x y =
-    prove_goal thy x
+    prove_goal (the_context ()) x
       (fn [prem] => [(rtac cut 1), (rtac y 2), (rtac prem 2),
-	 	     (best_tac lazy_cs 1)]);
+                     (best_tac lazy_cs 1)]);
 
 val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1,
-				 contrad2, mp_rule1, mp_rule2, o_a_rule,
-				 a_not_a_rule]
-		      add_unsafes [aux_impl];
+                                 contrad2, mp_rule1, mp_rule2, o_a_rule,
+                                 a_not_a_rule]
+                      add_unsafes [aux_impl];
 
 val power_cs = safe_cs add_unsafes [impr_contr_der];
 
-fun auto1 x = prove_goal thy x (fn prems => [best_tac safe_cs 1]) ;
+fun auto1 x = prove_goal (the_context ()) x (fn prems => [best_tac safe_cs 1]) ;
 
-fun auto2 x = prove_goal thy x (fn prems => [best_tac power_cs 1]) ;
+fun auto2 x = prove_goal (the_context ()) x (fn prems => [best_tac power_cs 1]) ;
 
 
 (* some examples from Troelstra and van Dalen
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,11 +1,12 @@
-(*  Title:      ILL.thy
+(*  Title:      Sequents/ILL.thy
     ID:         $Id$
     Author:     Sara Kalvala and Valeria de Paiva
     Copyright   1995  University of Cambridge
 *)
 
-
-ILL = Sequents +
+theory ILL
+imports Sequents
+begin
 
 consts
   Trueprop       :: "two_seqi"
@@ -35,98 +36,93 @@
   "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
   "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")
 
+parse_translation {*
+  [("@Trueprop", single_tr "Trueprop"),
+   ("@Context", two_seq_tr "Context"),
+   ("@PromAux", three_seq_tr "PromAux")] *}
+
+print_translation {*
+  [("Trueprop", single_tr' "@Trueprop"),
+   ("Context", two_seq_tr'"@Context"),
+   ("PromAux", three_seq_tr'"@PromAux")] *}
+
 defs
 
-liff_def        "P o-o Q == (P -o Q) >< (Q -o P)"
+liff_def:        "P o-o Q == (P -o Q) >< (Q -o P)"
 
-aneg_def        "~A == A -o 0"
+aneg_def:        "~A == A -o 0"
 
 
-
-
-rules
+axioms
 
-identity        "P |- P"
+identity:        "P |- P"
 
-zerol           "$G, 0, $H |- A"
+zerol:           "$G, 0, $H |- A"
 
   (* RULES THAT DO NOT DIVIDE CONTEXT *)
 
-derelict   "$F, A, $G |- C ==> $F, !A, $G |- C"
+derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C"
   (* unfortunately, this one removes !A  *)
 
-contract  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
+contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
 
-weaken     "$F, $G |- C ==> $G, !A, $F |- C"
+weaken:     "$F, $G |- C ==> $G, !A, $F |- C"
   (* weak form of weakening, in practice just to clean context *)
   (* weaken and contract not needed (CHECK)  *)
 
-promote2        "promaux{ || $H || B} ==> $H |- !B"
-promote1        "promaux{!A, $G || $H || B}
-                 ==> promaux {$G || $H, !A || B}"
-promote0        "$G |- A ==> promaux {$G || || A}"
+promote2:        "promaux{ || $H || B} ==> $H |- !B"
+promote1:        "promaux{!A, $G || $H || B}
+                  ==> promaux {$G || $H, !A || B}"
+promote0:        "$G |- A ==> promaux {$G || || A}"
 
 
 
-tensl     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
+tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
 
-impr      "A, $F |- B ==> $F |- A -o B"
+impr:      "A, $F |- B ==> $F |- A -o B"
 
-conjr           "[| $F |- A ;
+conjr:           "[| $F |- A ;
                  $F |- B |]
                 ==> $F |- (A && B)"
 
-conjll          "$G, A, $H |- C ==> $G, A && B, $H |- C"
+conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C"
 
-conjlr          "$G, B, $H |- C ==> $G, A && B, $H |- C"
+conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C"
 
-disjrl          "$G |- A ==> $G |- A ++ B"
-disjrr          "$G |- B ==> $G |- A ++ B"
-disjl           "[| $G, A, $H |- C ;
-                    $G, B, $H |- C |]
-                ==> $G, A ++ B, $H |- C"
+disjrl:          "$G |- A ==> $G |- A ++ B"
+disjrr:          "$G |- B ==> $G |- A ++ B"
+disjl:           "[| $G, A, $H |- C ;
+                     $G, B, $H |- C |]
+                 ==> $G, A ++ B, $H |- C"
 
 
       (* RULES THAT DIVIDE CONTEXT *)
 
-tensr           "[| $F, $J :=: $G;
-                    $F |- A ;
-                    $J |- B     |]
-                    ==> $G |- A >< B"
+tensr:           "[| $F, $J :=: $G;
+                     $F |- A ;
+                     $J |- B     |]
+                     ==> $G |- A >< B"
 
-impl            "[| $G, $F :=: $J, $H ;
-                    B, $F |- C ;
-                       $G |- A |]
-                    ==> $J, A -o B, $H |- C"
+impl:            "[| $G, $F :=: $J, $H ;
+                     B, $F |- C ;
+                        $G |- A |]
+                     ==> $J, A -o B, $H |- C"
 
 
-cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
-         $H1, $H2, $H3, $H4 |- A ;
-         $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
+cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
+          $H1, $H2, $H3, $H4 |- A ;
+          $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
 
 
   (* CONTEXT RULES *)
 
-context1     "$G :=: $G"
-context2     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
-context3     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
-context4a    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
-context4b    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
-context5     "$F, $G :=: $H ==> $G, $F :=: $H"
+context1:     "$G :=: $G"
+context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
+context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
+context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
+context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
+context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
 
-
-
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
-
-ML
-
-val parse_translation = [("@Trueprop",Sequents.single_tr "Trueprop"),
-                         ("@Context",Sequents.two_seq_tr "Context"),
-                         ("@PromAux", Sequents.three_seq_tr "PromAux")];
-
-val print_translation = [("Trueprop",Sequents.single_tr' "@Trueprop"),
-                         ("Context",Sequents.two_seq_tr'"@Context"),
-                         ("PromAux", Sequents.three_seq_tr'"@PromAux")];
-
-
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/ILL/ILL_predlog.ML
--- a/src/Sequents/ILL/ILL_predlog.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/ILL_predlog.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -1,6 +1,6 @@
 
-fun auto1 x = prove_goal thy x
+fun auto1 x = prove_goal (the_context ()) x
  (fn prems => [best_tac safe_cs 1]) ;
 
-fun auto2 x = prove_goal thy x
+fun auto2 x = prove_goal (the_context ()) x
  (fn prems => [best_tac power_cs 1]) ;
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/ILL/ILL_predlog.thy
--- a/src/Sequents/ILL/ILL_predlog.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/ILL_predlog.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,36 +1,32 @@
-(* 
-    File:	 /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy
-    Theory Name: pred_log
-    Logic Image: HOL
-*)
+(* $Id$ *)
 
-ILL_predlog  =  ILL +
+theory ILL_predlog
+imports ILL
+begin
 
-types
-    plf
-    
+typedecl plf
+
 consts
-
   "&"   :: "[plf,plf] => plf"   (infixr 35)
   "|"   :: "[plf,plf] => plf"   (infixr 35)
   ">"   :: "[plf,plf] => plf"   (infixr 35)
   "="   :: "[plf,plf] => plf"   (infixr 35)
   "@NG" :: "plf => plf"   ("- _ " [50] 55)
   ff    :: "plf"
-  
+
   PL    :: "plf => o"      ("[* / _ / *]" [] 100)
 
 
 translations
 
-  "[* A & B *]" == "[*A*] && [*B*]" 
+  "[* A & B *]" == "[*A*] && [*B*]"
   "[* A | B *]" == "![*A*] ++ ![*B*]"
   "[* - A *]"   == "[*A > ff*]"
   "[* ff *]"    == "0"
   "[* A = B *]" => "[* (A > B) & (B > A) *]"
-  
+
   "[* A > B *]" == "![*A*] -o [*B*]"
-  
+
 (* another translations for linear implication:
   "[* A > B *]" == "!([*A*] -o [*B*])" *)
 
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/ILL/ROOT.ML
--- a/src/Sequents/ILL/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/ROOT.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -1,3 +1,4 @@
+(* $Id$ *)
 
 time_use_thy "washing";
 time_use_thy "ILL_predlog";
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/ILL/washing.ML
--- a/src/Sequents/ILL/washing.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/washing.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -1,3 +1,5 @@
+(* $Id$ *)
+
 (* "activate" definitions for use in proof *)
 
 val changeI = [context1] RL ([change] RLN (2,[cut]));
@@ -16,15 +18,11 @@
 
 (* order of premises doesn't matter *)
 
-prove_goal thy "dollar , dirty , dollar |- clean"
+prove_goal (the_context ()) "dollar , dirty , dollar |- clean"
 (fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
 
 
 (* alternative formulation *)
 
-prove_goal thy "dollar , dollar |- dirty -o clean"
+prove_goal (the_context ()) "dollar , dollar |- dirty -o clean"
 (fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
-
-
-
-
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/ILL/washing.thy
--- a/src/Sequents/ILL/washing.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/washing.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,33 +1,38 @@
-
 
-(* code by Sara Kalvala, based on Paulson's LK 
+(* $Id$ *)
+
+(* code by Sara Kalvala, based on Paulson's LK
                            and Moore's tisl.ML *)
 
-washing = ILL +
+theory washing
+imports ILL
+begin
 
 consts
-
-dollar,quarter,loaded,dirty,wet,clean        :: "o"			
+  dollar :: o
+  quarter :: o
+  loaded :: o
+  dirty :: o
+  wet :: o
+  clean :: o
 
-  
-rules
-
-
-  change
+axioms
+  change:
   "dollar |- (quarter >< quarter >< quarter >< quarter)"
 
-  load1
+  load1:
   "quarter , quarter , quarter , quarter , quarter |- loaded"
 
-  load2
+  load2:
   "dollar , quarter |- loaded"
 
-  wash
+  wash:
   "loaded , dirty |- wet"
 
-  dry
+  dry:
   "wet, quarter , quarter , quarter |- clean"
 
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
 
-  
\ No newline at end of file
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,4 +1,4 @@
-(*  Title:      LK/LK
+(*  Title:      LK/LK.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -13,12 +13,20 @@
 various modal rules would become inconsistent.
 *)
 
-LK = LK0 +
+theory LK
+imports LK0
+uses ("simpdata.ML")
+begin
 
-rules
+axioms
+
+  monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
 
-  monotonic  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
+  left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
+               ==> (P, $H |- $F) == (P', $H' |- $F')"
 
-  left_cong  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |] 
-              ==> (P, $H |- $F) == (P', $H' |- $F')"
+ML {* use_legacy_bindings (the_context ()) *}
+
+use "simpdata.ML"
+
 end
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/LK/Nat.ML
--- a/src/Sequents/LK/Nat.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/Nat.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -1,9 +1,7 @@
-(*  Title:      Sequents/LK/Nat
+(*  Title:      Sequents/LK/Nat.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
-
-Theory of the natural numbers: Peano's axioms, primitive recursion
 *)
 
 Addsimps [Suc_neq_0];
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/Nat.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,26 +1,32 @@
-(*  Title:      Sequents/LK/Nat
+(*  Title:      Sequents/LK/Nat.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
-
-Theory of the natural numbers: Peano's axioms, primitive recursion
 *)
 
-Nat = LK +
-types   nat
-arities nat :: term
+header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
+
+theory Nat
+imports LK
+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)
+        Suc :: "nat=>nat"
+        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
+        "+" :: "[nat, nat] => nat"                (infixl 60)
 
-rules   
-  induct  "[| $H |- $E, P(0), $F;
+axioms
+  induct:  "[| $H |- $E, P(0), $F;
               !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
 
-  Suc_inject  "|- Suc(m)=Suc(n) --> m=n"
-  Suc_neq_0   "|- Suc(m) ~= 0"
-  rec_0       "|- rec(0,a,f) = a"
-  rec_Suc     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
-  add_def     "m+n == rec(m, n, %x y. Suc(y))"
+  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n"
+  Suc_neq_0:   "|- Suc(m) ~= 0"
+  rec_0:       "|- rec(0,a,f) = a"
+  rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
+  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/LK/ROOT.ML
--- a/src/Sequents/LK/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/ROOT.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Executes all examples for Classical Logic. 
+Examples for Classical Logic.
 *)
 
 time_use "prop.ML";
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/LK/hardquant.ML
--- a/src/Sequents/LK/hardquant.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/hardquant.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -12,25 +12,23 @@
 Uses pc_tac rather than fast_tac when the former is significantly faster.
 *)
 
-writeln"File LK/ex/hard-quant.";
-
-context LK.thy;
+context (theory "LK");
 
 Goal "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
 by (Fast_tac 1);
-result(); 
+result();
 
 Goal "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
 by (Fast_tac 1);
-result(); 
+result();
 
 Goal "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
 by (Fast_tac 1);
-result(); 
+result();
 
 Goal "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
 by (Fast_tac 1);
-result(); 
+result();
 
 writeln"Problems requiring quantifier duplication";
 
@@ -53,7 +51,7 @@
 writeln"Problem 18";
 Goal "|- EX y. ALL x. P(y)-->P(x)";
 by (best_tac LK_dup_pack 1);
-result(); 
+result();
 
 writeln"Problem 19";
 Goal "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
@@ -63,7 +61,7 @@
 writeln"Problem 20";
 Goal "|- (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 1); 
+by (Fast_tac 1);
 result();
 
 writeln"Problem 21";
@@ -73,12 +71,12 @@
 
 writeln"Problem 22";
 Goal "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
-by (Fast_tac 1); 
+by (Fast_tac 1);
 result();
 
 writeln"Problem 23";
 Goal "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
-by (best_tac LK_pack 1);  
+by (best_tac LK_pack 1);
 result();
 
 writeln"Problem 24";
@@ -94,7 +92,7 @@
 \       (ALL x. P(x) --> (M(x) & L(x))) &   \
 \       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
 \   --> (EX x. Q(x)&P(x))";
-by (best_tac LK_pack 1);  
+by (best_tac LK_pack 1);
 result();
 
 writeln"Problem 26";
@@ -110,7 +108,7 @@
 \             (ALL x. M(x) & L(x) --> P(x)) &   \
 \             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
 \         --> (ALL x. M(x) --> ~L(x))";
-by (pc_tac LK_pack 1); 
+by (pc_tac LK_pack 1);
 result();
 
 writeln"Problem 28.  AMENDED";
@@ -118,21 +116,21 @@
 \       ((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))";
-by (pc_tac LK_pack 1);  
+by (pc_tac LK_pack 1);
 result();
 
 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
 Goal "|- (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 (pc_tac LK_pack 1); 
+by (pc_tac LK_pack 1);
 result();
 
 writeln"Problem 30";
 Goal "|- (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 1);  
+by (Fast_tac 1);
 result();
 
 writeln"Problem 31";
@@ -238,7 +236,7 @@
 \     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
 \                  & (ALL y. g(y) & h(x,y) --> j(x,y)))         \
 \     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
-by (best_tac LK_pack 1); 
+by (best_tac LK_pack 1);
 result();
 
 
@@ -249,7 +247,7 @@
 by (fast_tac (pack() add_safes [subst]) 1);
 result();
 
-writeln"Problem 50";  
+writeln"Problem 50";
 Goal "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
 by (best_tac LK_dup_pack 1);
 result();
@@ -287,7 +285,7 @@
 writeln"Problem 59";
 (*Unification works poorly here -- the abstraction %sobj prevents efficient
   operation of the occurs check*)
-Unify.trace_bound := !Unify.search_bound - 1; 
+Unify.trace_bound := !Unify.search_bound - 1;
 Goal "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
 by (best_tac LK_dup_pack 1);
 result();
@@ -304,8 +302,7 @@
 by (Fast_tac 1);
 result();
 
-writeln"Reached end of file.";
-
 (*18 June 92: loaded in 372 secs*)
 (*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
 (*29 June 92: loaded in 370 secs*)
+(*18 September 2005: loaded in 1.809 secs*)
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/LK/prop.ML
--- a/src/Sequents/LK/prop.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/prop.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -7,93 +7,91 @@
 Can be read to test the LK system.
 *)
 
-writeln"LK/ex/prop: propositional examples";
-
 writeln"absorptive laws of & and | ";
 
-goal LK.thy "|- P & P <-> P";
+goal (theory "LK") "|- P & P <-> P";
 by (fast_tac prop_pack 1);
 result();
 
-goal LK.thy "|- P | P <-> P";
+goal (theory "LK") "|- P | P <-> P";
 by (fast_tac prop_pack 1);
 result();
 
 writeln"commutative laws of & and | ";
 
-goal LK.thy "|- P & Q  <->  Q & P";
+goal (theory "LK") "|- P & Q  <->  Q & P";
 by (fast_tac prop_pack 1);
 result();
 
-goal LK.thy "|- P | Q  <->  Q | P";
+goal (theory "LK") "|- P | Q  <->  Q | P";
 by (fast_tac prop_pack 1);
 result();
 
 
 writeln"associative laws of & and | ";
 
-goal LK.thy "|- (P & Q) & R  <->  P & (Q & R)";
+goal (theory "LK") "|- (P & Q) & R  <->  P & (Q & R)";
 by (fast_tac prop_pack 1);
 result();
 
-goal LK.thy "|- (P | Q) | R  <->  P | (Q | R)";
+goal (theory "LK") "|- (P | Q) | R  <->  P | (Q | R)";
 by (fast_tac prop_pack 1);
 result();
 
 writeln"distributive laws of & and | ";
-goal LK.thy "|- (P & Q) | R  <-> (P | R) & (Q | R)";
+goal (theory "LK") "|- (P & Q) | R  <-> (P | R) & (Q | R)";
 by (fast_tac prop_pack 1);
 result();
 
-goal LK.thy "|- (P | Q) & R  <-> (P & R) | (Q & R)";
+goal (theory "LK") "|- (P | Q) & R  <-> (P & R) | (Q & R)";
 by (fast_tac prop_pack 1);
 result();
 
 writeln"Laws involving implication";
 
-goal LK.thy "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
+goal (theory "LK") "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
 by (fast_tac prop_pack 1);
 result(); 
 
-goal LK.thy "|- (P & Q --> R) <-> (P--> (Q-->R))";
+goal (theory "LK") "|- (P & Q --> R) <-> (P--> (Q-->R))";
 by (fast_tac prop_pack 1);
 result(); 
 
 
-goal LK.thy "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
+goal (theory "LK") "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
 by (fast_tac prop_pack 1);
 result();
 
 
 writeln"Classical theorems";
 
-goal LK.thy "|- P|Q --> P| ~P&Q";
+goal (theory "LK") "|- P|Q --> P| ~P&Q";
 by (fast_tac prop_pack 1);
 result();
 
 
-goal LK.thy "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
+goal (theory "LK") "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
 by (fast_tac prop_pack 1);
 result();
 
 
-goal LK.thy "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
+goal (theory "LK") "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
 by (fast_tac prop_pack 1);
 result();
 
 
-goal LK.thy "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
+goal (theory "LK") "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
 by (fast_tac prop_pack 1);
 result();
 
 
 (*If and only if*)
 
-goal LK.thy "|- (P<->Q) <-> (Q<->P)";
+goal (theory "LK") "|- (P<->Q) <-> (Q<->P)";
 by (fast_tac prop_pack 1);
 result();
 
-goal LK.thy "|- ~ (P <-> ~P)";
+goal (theory "LK") "|- ~ (P <-> ~P)";
 by (fast_tac prop_pack 1);
 result();
 
@@ -106,89 +104,87 @@
 *)
 
 (*1*)
-goal LK.thy "|- (P-->Q)  <->  (~Q --> ~P)";
+goal (theory "LK") "|- (P-->Q)  <->  (~Q --> ~P)";
 by (fast_tac prop_pack 1);
 result();
 
 (*2*)
-goal LK.thy "|- ~ ~ P  <->  P";
+goal (theory "LK") "|- ~ ~ P  <->  P";
 by (fast_tac prop_pack 1);
 result();
 
 (*3*)
-goal LK.thy "|- ~(P-->Q) --> (Q-->P)";
+goal (theory "LK") "|- ~(P-->Q) --> (Q-->P)";
 by (fast_tac prop_pack 1);
 result();
 
 (*4*)
-goal LK.thy "|- (~P-->Q)  <->  (~Q --> P)";
+goal (theory "LK") "|- (~P-->Q)  <->  (~Q --> P)";
 by (fast_tac prop_pack 1);
 result();
 
 (*5*)
-goal LK.thy "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
+goal (theory "LK") "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
 by (fast_tac prop_pack 1);
 result();
 
 (*6*)
-goal LK.thy "|- P | ~ P";
+goal (theory "LK") "|- P | ~ P";
 by (fast_tac prop_pack 1);
 result();
 
 (*7*)
-goal LK.thy "|- P | ~ ~ ~ P";
+goal (theory "LK") "|- P | ~ ~ ~ P";
 by (fast_tac prop_pack 1);
 result();
 
 (*8.  Peirce's law*)
-goal LK.thy "|- ((P-->Q) --> P)  -->  P";
+goal (theory "LK") "|- ((P-->Q) --> P)  -->  P";
 by (fast_tac prop_pack 1);
 result();
 
 (*9*)
-goal LK.thy "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
+goal (theory "LK") "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
 by (fast_tac prop_pack 1);
 result();
 
 (*10*)
-goal LK.thy "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
+goal (theory "LK") "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
 by (fast_tac prop_pack 1);
 result();
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
-goal LK.thy "|- P<->P";
+goal (theory "LK") "|- P<->P";
 by (fast_tac prop_pack 1);
 result();
 
 (*12.  "Dijkstra's law"*)
-goal LK.thy "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
+goal (theory "LK") "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
 by (fast_tac prop_pack 1);
 result();
 
 (*13.  Distributive law*)
-goal LK.thy "|- P | (Q & R)  <-> (P | Q) & (P | R)";
+goal (theory "LK") "|- P | (Q & R)  <-> (P | Q) & (P | R)";
 by (fast_tac prop_pack 1);
 result();
 
 (*14*)
-goal LK.thy "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
+goal (theory "LK") "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
 by (fast_tac prop_pack 1);
 result();
 
 
 (*15*)
-goal LK.thy "|- (P --> Q) <-> (~P | Q)";
+goal (theory "LK") "|- (P --> Q) <-> (~P | Q)";
 by (fast_tac prop_pack 1);
 result();
 
 (*16*)
-goal LK.thy "|- (P-->Q) | (Q-->P)";
+goal (theory "LK") "|- (P-->Q) | (Q-->P)";
 by (fast_tac prop_pack 1);
 result();
 
 (*17*)
-goal LK.thy "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
+goal (theory "LK") "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
 by (fast_tac prop_pack 1);
 result();
-
-writeln"Reached end of file.";
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/LK/quant.ML
--- a/src/Sequents/LK/quant.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/quant.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -1,4 +1,4 @@
-(*  Title:      LK/ex/quant
+(*  Title:      LK/ex/quant.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
@@ -6,155 +6,151 @@
 Classical sequent calculus: examples with quantifiers.
 *)
 
-
-writeln"LK/ex/quant: Examples with quantifiers";
-
-goal LK.thy "|- (ALL x. P)  <->  P";
+goal (theory "LK") "|- (ALL x. P)  <->  P";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
-goal LK.thy "|- (ALL x y. P(x,y))  <->  (ALL y x. P(x,y))";
+goal (theory "LK") "|- (ALL x y. P(x,y))  <->  (ALL y x. P(x,y))";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
-goal LK.thy "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)";
+goal (theory "LK") "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
 writeln"Permutation of existential quantifier.";
-goal LK.thy "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))";
+goal (theory "LK") "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
-goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
+goal (theory "LK") "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
 
 (*Converse is invalid*)
-goal LK.thy "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
+goal (theory "LK") "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
 
 writeln"Pushing ALL into an implication.";
-goal LK.thy "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))";
+goal (theory "LK") "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
 
-goal LK.thy "|- (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
+goal (theory "LK") "|- (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
 
-goal LK.thy "|- (EX x. P)  <->  P";
+goal (theory "LK") "|- (EX x. P)  <->  P";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
 
 writeln"Distribution of EX over disjunction.";
-goal LK.thy "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))";
+goal (theory "LK") "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 (*5 secs*)
 
 (*Converse is invalid*)
-goal LK.thy "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))";
+goal (theory "LK") "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
 
 writeln"Harder examples: classical theorems.";
 
-goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
+goal (theory "LK") "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 (*3 secs*)
 
 
-goal LK.thy "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
+goal (theory "LK") "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 (*5 secs*)
 
 
-goal LK.thy "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
+goal (theory "LK") "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
 by (fast_tac LK_pack 1);
-result(); 
+result();
 
 
 writeln"Basic test of quantifier reasoning";
-goal LK.thy
+goal (theory "LK")
    "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
 by (fast_tac LK_pack 1);
-result();  
+result();
 
 
-goal LK.thy "|- (ALL x. Q(x))  -->  (EX x. Q(x))";
+goal (theory "LK") "|- (ALL x. Q(x))  -->  (EX x. Q(x))";
 by (fast_tac LK_pack 1);
-result();  
+result();
 
 
 writeln"The following are invalid!";
 
 (*INVALID*)
-goal LK.thy "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
-by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; 
+goal (theory "LK") "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
+by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
 (*Check that subgoals remain: proof failed.*)
-getgoal 1; 
+getgoal 1;
 
 (*INVALID*)
-goal LK.thy "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
+goal (theory "LK") "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
-getgoal 1; 
+getgoal 1;
 
-goal LK.thy "|- P(?a) --> (ALL x. P(x))";
+goal (theory "LK") "|- P(?a) --> (ALL x. P(x))";
 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
 (*Check that subgoals remain: proof failed.*)
-getgoal 1;  
+getgoal 1;
 
-goal LK.thy "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
+goal (theory "LK") "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
-getgoal 1;  
+getgoal 1;
 
 
 writeln"Back to things that are provable...";
 
-goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
-by (fast_tac LK_pack 1); 
-result();  
+goal (theory "LK") "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
+by (fast_tac LK_pack 1);
+result();
 
 (*An example of why exR should be delayed as long as possible*)
-goal LK.thy "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))";
+goal (theory "LK") "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))";
 by (fast_tac LK_pack 1);
-result();  
+result();
 
 writeln"Solving for a Var";
-goal LK.thy 
+goal (theory "LK")
    "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
 by (fast_tac LK_pack 1);
 result();
 
 
 writeln"Principia Mathematica *11.53";
-goal LK.thy 
+goal (theory "LK")
     "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
 by (fast_tac LK_pack 1);
 result();
 
 
 writeln"Principia Mathematica *11.55";
-goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
+goal (theory "LK") "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
 by (fast_tac LK_pack 1);
 result();
 
 writeln"Principia Mathematica *11.61";
-goal LK.thy
+goal (theory "LK")
    "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
 by (fast_tac LK_pack 1);
 result();
 
-writeln"Reached end of file.";
-
 (*21 August 88: loaded in 45.7 secs*)
+(*18 September 2005: loaded in 0.114 secs*)
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/LK0.ML
--- a/src/Sequents/LK0.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK0.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -1,9 +1,9 @@
-(*  Title:      LK/LK0
+(*  Title:      LK/LK0.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Tactics and lemmas for LK (thanks also to Philippe de Groote)  
+Tactics and lemmas for LK (thanks also to Philippe de Groote)
 
 Structural rules by Soren Heilmann
 *)
@@ -41,21 +41,21 @@
 qed "exchL";
 
 (*Cut and thin, replacing the right-side formula*)
-fun cutR_tac (sP: string) i = 
+fun cutR_tac (sP: string) i =
     res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
 
 (*Cut and thin, replacing the left-side formula*)
-fun cutL_tac (sP: string) i = 
+fun cutL_tac (sP: string) i =
     res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
 
 
 (** If-and-only-if rules **)
-Goalw [iff_def] 
+Goalw [iff_def]
     "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F";
 by (REPEAT (ares_tac [conjR,impR] 1));
 qed "iffR";
 
-Goalw [iff_def] 
+Goalw [iff_def]
     "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E";
 by (REPEAT (ares_tac [conjL,impL,basic] 1));
 qed "iffL";
@@ -93,31 +93,31 @@
 
 
 (*The rules of LK*)
-val prop_pack = empty_pack add_safes 
-                [basic, refl, TrueR, FalseL, 
-		 conjL, conjR, disjL, disjR, impL, impR, 
+val prop_pack = empty_pack add_safes
+                [basic, refl, TrueR, FalseL,
+                 conjL, conjR, disjL, disjR, impL, impR,
                  notL, notR, iffL, iffR];
 
-val LK_pack = prop_pack add_safes   [allR, exL] 
+val LK_pack = prop_pack add_safes   [allR, exL]
                         add_unsafes [allL_thin, exR_thin, the_equality];
 
-val LK_dup_pack = prop_pack add_safes   [allR, exL] 
+val LK_dup_pack = prop_pack add_safes   [allR, exL]
                             add_unsafes [allL, exR, the_equality];
 
 
 pack_ref() := LK_pack;
 
-fun lemma_tac th i = 
+fun lemma_tac th i =
     rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
 
-val [major,minor] = goal thy 
+val [major,minor] = goal (the_context ())
     "[| $H |- $E, $F, P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
 by (rtac (thinRS RS cut) 1 THEN rtac major 1);
 by (Step_tac 1);
 by (rtac thinR 1 THEN rtac minor 1);
 qed "mp_R";
 
-val [major,minor] = goal thy 
+val [major,minor] = goal (the_context ())
     "[| $H, $G |- $E, P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
 by (rtac (thinL RS cut) 1 THEN rtac major 1);
 by (Step_tac 1);
@@ -127,14 +127,14 @@
 
 (** Two rules to generate left- and right- rules from implications **)
 
-val [major,minor] = goal thy 
+val [major,minor] = goal (the_context ())
     "[| |- P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
 by (rtac mp_R 1);
 by (rtac minor 2);
 by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
 qed "R_of_imp";
 
-val [major,minor] = goal thy 
+val [major,minor] = goal (the_context ())
     "[| |- P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
 by (rtac mp_L 1);
 by (rtac minor 2);
@@ -142,7 +142,7 @@
 qed "L_of_imp";
 
 (*Can be used to create implications in a subgoal*)
-val [prem] = goal thy 
+val [prem] = goal (the_context ())
     "[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F";
 by (rtac mp_L 1);
 by (rtac basic 2);
@@ -151,17 +151,17 @@
 
 Goal "|-P&Q ==> |-P";
 by (etac (thinR RS cut) 1);
-by (Fast_tac 1);		
+by (Fast_tac 1);
 qed "conjunct1";
 
 Goal "|-P&Q ==> |-Q";
 by (etac (thinR RS cut) 1);
-by (Fast_tac 1);		
+by (Fast_tac 1);
 qed "conjunct2";
 
 Goal "|- (ALL x. P(x)) ==> |- P(x)";
 by (etac (thinR RS cut) 1);
-by (Fast_tac 1);		
+by (Fast_tac 1);
 qed "spec";
 
 (** Equality **)
@@ -189,12 +189,12 @@
 (* Two theorms for rewriting only one instance of a definition:
    the first for definitions of formulae and the second for terms *)
 
-val prems = goal thy "(A == B) ==> |- A <-> B";
+val prems = goal (the_context ()) "(A == B) ==> |- A <-> B";
 by (rewrite_goals_tac prems);
 by (rtac iff_refl 1);
 qed "def_imp_iff";
 
-val prems = goal thy "(A == B) ==> |- A = B";
+val prems = goal (the_context ()) "(A == B) ==> |- A = B";
 by (rewrite_goals_tac prems);
 by (rtac refl 1);
 qed "meta_eq_to_obj_eq";
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK0.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,136 +1,139 @@
-(*  Title:      LK/LK0
+(*  Title:      LK/LK0.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Classical First-Order Sequent Calculus
-
 There may be printing problems if a seqent is in expanded normal form
-	(eta-expanded, beta-contracted)
+        (eta-expanded, beta-contracted)
 *)
 
-LK0 = Sequents +
+header {* Classical First-Order Sequent Calculus *}
+
+theory LK0
+imports Sequents
+begin
 
 global
 
-classes term
-default term
+classes "term"
+defaultsort "term"
 
 consts
 
- Trueprop	:: "two_seqi"
+ Trueprop       :: "two_seqi"
 
-  True,False   :: o
-  "="          :: ['a,'a] => o       (infixl 50)
-  Not          :: o => o             ("~ _" [40] 40)
-  "&"          :: [o,o] => o         (infixr 35)
-  "|"          :: [o,o] => o         (infixr 30)
-  "-->","<->"  :: [o,o] => o         (infixr 25)
-  The          :: ('a => o) => 'a    (binder "THE " 10)
-  All          :: ('a => o) => o     (binder "ALL " 10)
-  Ex           :: ('a => o) => o     (binder "EX " 10)
+  True         :: o
+  False        :: o
+  "="          :: "['a,'a] => o"     (infixl 50)
+  Not          :: "o => o"           ("~ _" [40] 40)
+  "&"          :: "[o,o] => o"       (infixr 35)
+  "|"          :: "[o,o] => o"       (infixr 30)
+  "-->"        :: "[o,o] => o"       (infixr 25)
+  "<->"        :: "[o,o] => o"       (infixr 25)
+  The          :: "('a => o) => 'a"  (binder "THE " 10)
+  All          :: "('a => o) => o"   (binder "ALL " 10)
+  Ex           :: "('a => o) => o"   (binder "EX " 10)
 
 syntax
- "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
-  "_not_equal" :: ['a, 'a] => o                (infixl "~=" 50)
+ "@Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
+  "_not_equal" :: "['a, 'a] => o"              (infixl "~=" 50)
+
+parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
+print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
 
 translations
   "x ~= y"      == "~ (x = y)"
 
 syntax (xsymbols)
-  Not           :: o => o               ("\\<not> _" [40] 40)
-  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
-  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
-  "op -->"      :: [o, o] => o          (infixr "\\<longrightarrow>" 25)
-  "op <->"      :: [o, o] => o          (infixr "\\<longleftrightarrow>" 25)
-  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
-  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
-  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
-  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
+  Not           :: "o => o"               ("\<not> _" [40] 40)
+  "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
+  "op |"        :: "[o, o] => o"          (infixr "\<or>" 30)
+  "op -->"      :: "[o, o] => o"          (infixr "\<longrightarrow>" 25)
+  "op <->"      :: "[o, o] => o"          (infixr "\<longleftrightarrow>" 25)
+  "ALL "        :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
+  "EX "         :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
+  "EX! "        :: "[idts, o] => o"       ("(3\<exists>!_./ _)" [0, 10] 10)
+  "_not_equal"  :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
 
 syntax (HTML output)
-  Not           :: o => o               ("\\<not> _" [40] 40)
-  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
-  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
-  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
-  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
-  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
-  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
-
+  Not           :: "o => o"               ("\<not> _" [40] 40)
+  "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
+  "op |"        :: "[o, o] => o"          (infixr "\<or>" 30)
+  "ALL "        :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
+  "EX "         :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
+  "EX! "        :: "[idts, o] => o"       ("(3\<exists>!_./ _)" [0, 10] 10)
+  "_not_equal"  :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
 
 local
-  
-rules
+
+axioms
 
   (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
 
-  contRS "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F"
-  contLS "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
+  contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F"
+  contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
 
-  thinRS "$H |- $E, $F ==> $H |- $E, $S, $F"
-  thinLS "$H, $G |- $E ==> $H, $S, $G |- $E"
+  thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F"
+  thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E"
 
-  exchRS "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F"
-  exchLS "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
+  exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F"
+  exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
 
-  cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
+  cut:   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
 
   (*Propositional rules*)
 
-  basic "$H, P, $G |- $E, P, $F"
+  basic: "$H, P, $G |- $E, P, $F"
 
-  conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
-  conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
+  conjR: "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
+  conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
 
-  disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
-  disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
+  disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
+  disjL: "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
 
-  impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
-  impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
+  impR:  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
+  impL:  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
 
-  notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
-  notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
+  notR:  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
+  notL:  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
 
-  FalseL "$H, False, $G |- $E"
+  FalseL: "$H, False, $G |- $E"
 
-  True_def "True == False-->False"
-  iff_def  "P<->Q == (P-->Q) & (Q-->P)"
+  True_def: "True == False-->False"
+  iff_def:  "P<->Q == (P-->Q) & (Q-->P)"
 
   (*Quantifiers*)
 
-  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
-  allL  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
+  allR:  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
+  allL:  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
 
-  exR   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
-  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
+  exR:   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
+  exL:   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
 
   (*Equality*)
 
-  refl  "$H |- $E, a=a, $F"
-  subst "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
+  refl:  "$H |- $E, a=a, $F"
+  subst: "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
 
   (* Reflection *)
 
-  eq_reflection  "|- x=y ==> (x==y)"
-  iff_reflection "|- P<->Q ==> (P==Q)"
+  eq_reflection:  "|- x=y ==> (x==y)"
+  iff_reflection: "|- P<->Q ==> (P==Q)"
 
   (*Descriptions*)
 
-  The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
+  The: "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
           $H |- $E, P(THE x. P(x)), $F"
 
 constdefs
-  If :: [o, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
+  If :: "[o, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
    "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
 
 setup
   prover_setup
 
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
 
-ML
 
-
-val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
-val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
-
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/Modal/ROOT.ML
--- a/src/Sequents/Modal/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/Modal/ROOT.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -1,21 +1,21 @@
-(*  Title:      Modal/ex/ROOT
+(*  Title:      Modal/ex/ROOT.ML
     ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
 
 writeln "\nTheorems of T\n";
-fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
+fun try s = (writeln s; prove_goal (theory "T") s (fn _=> [T_Prover.solve_tac 2]));
 time_use "Tthms.ML";
 
 writeln "\nTheorems of S4\n";
-fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2]));
+fun try s = (writeln s; prove_goal (theory "S4") s (fn _=> [S4_Prover.solve_tac 2]));
 time_use "Tthms.ML";
 time_use "S4thms.ML";
 
 writeln "\nTheorems of S43\n";
 fun try s = (writeln s;
-             prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE 
+             prove_goal (theory "S43") s (fn _=> [S43_Prover.solve_tac 2 ORELSE
                                            S43_Prover.solve_tac 3]));
 time_use "Tthms.ML";
 time_use "S4thms.ML";
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/Modal0.ML
--- a/src/Sequents/Modal0.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/Modal0.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -4,19 +4,19 @@
     Copyright   1991  University of Cambridge
 *)
 
-structure Modal0_rls = 
+structure Modal0_rls =
 struct
 
-val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def];
+val rewrite_rls = [strimp_def,streqv_def];
 
 local
-  val iffR = prove_goal thy 
+  val iffR = prove_goal (the_context ())
       "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    (fn prems=>
     [ (rewtac iff_def),
       (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
 
-  val iffL = prove_goal thy 
+  val iffL = prove_goal (the_context ())
      "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    (fn prems=>
     [ rewtac iff_def,
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/Modal0.thy
--- a/src/Sequents/Modal0.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/Modal0.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,42 +1,43 @@
-(*  Title:      Sequents/Modal0
+(*  Title:      Sequents/Modal0.thy
     ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
 
-Modal0 = LK0 +
+theory Modal0
+imports LK0
+uses "modal.ML"
+begin
 
 consts
   box           :: "o=>o"       ("[]_" [50] 50)
   dia           :: "o=>o"       ("<>_" [50] 50)
-  "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
-  Lstar,Rstar   :: "two_seqi"
+  "--<"         :: "[o,o]=>o"   (infixr 25)
+  ">-<"         :: "[o,o]=>o"   (infixr 25)
+  Lstar         :: "two_seqi"
+  Rstar         :: "two_seqi"
 
 syntax
   "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
   "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
 
-rules
-  (* Definitions *)
-
-  strimp_def    "P --< Q == [](P --> Q)"
-  streqv_def    "P >-< Q == (P --< Q) & (Q --< P)"
-end
-
-ML
-
-local
-
+ML {*
   val Lstar = "Lstar";
   val Rstar = "Rstar";
   val SLstar = "@Lstar";
   val SRstar = "@Rstar";
 
-  fun star_tr c [s1,s2] =
-      Const(c,dummyT)$Sequents.seq_tr s1$Sequents.seq_tr s2;
-  fun star_tr' c [s1,s2] = 
-      Const(c,dummyT) $ Sequents.seq_tr' s1 $ Sequents.seq_tr' s2;
-in
-val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
-val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
-end;
+  fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
+  fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
+*}
+
+parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
+print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
+
+defs
+  strimp_def:    "P --< Q == [](P --> Q)"
+  streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
+end
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/ROOT.ML
--- a/src/Sequents/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ROOT.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -3,29 +3,18 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Adds Classical Sequent Calculus to a database containing pure Isabelle. 
+Classical Sequent Calculus based on Pure Isabelle. 
 *)
 
 val banner = "Sequent Calculii";
 writeln banner;
 
-print_depth 1;  
-
 Unify.trace_bound:= 20;
 Unify.search_bound := 40;
 
-use_thy "Sequents";
-use "prover.ML";
-
 use_thy "LK";
-use "simpdata.ML";
-
 use_thy "ILL";
-
-use "modal.ML";
 use_thy "Modal0";
 use_thy"T";
 use_thy"S4";
 use_thy"S43";
-
-print_depth 8;
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/S4.ML
--- a/src/Sequents/S4.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/S4.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -1,10 +1,10 @@
-(*  Title:      Modal/S4
+(*  Title:      Modal/S4.ML
     ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
 
-local open Modal0_rls S4
+local open Modal0_rls
 in structure MP_Rule : MODAL_PROVER_RULE =
    struct
     val rewrite_rls = rewrite_rls
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/S4.thy
--- a/src/Sequents/S4.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/S4.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,31 +1,37 @@
-(*  Title:      Modal/S4
+(*  Title:      Modal/S4.thy
     ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
 
-S4 = Modal0 +
-rules
+theory S4
+imports Modal0
+begin
+
+axioms
 (* Definition of the star operation using a set of Horn clauses *)
 (* For system S4:  gamma * == {[]P | []P : gamma}               *)
 (*                 delta * == {<>P | <>P : delta}               *)
 
-  lstar0         "|L>"
-  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
-  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
-  rstar0         "|R>"
-  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
-  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
+  lstar0:         "|L>"
+  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
+  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
+  rstar0:         "|R>"
+  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
+  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
 
 (* Rules for [] and <> *)
 
-  boxR
-   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
+  boxR:
+   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
            $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
-  boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
+  boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
 
-  diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
-  diaL
-   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
+  diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
+  diaL:
+   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
            $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/S43.ML
--- a/src/Sequents/S43.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/S43.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -2,11 +2,9 @@
     ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
-
-This implements Rajeev Gore's sequent calculus for S43.
 *)
 
-local open Modal0_rls S43
+local open Modal0_rls
 in structure MP_Rule : MODAL_PROVER_RULE =
    struct
     val rewrite_rls = rewrite_rls
@@ -16,4 +14,4 @@
     val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2]
    end;
 end;
-structure S43_Prover = Modal_ProverFun(MP_Rule);  
+structure S43_Prover = Modal_ProverFun(MP_Rule);
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/S43.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Modal/S43
+(*  Title:      Modal/S43.thy
     ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
@@ -6,7 +6,9 @@
 This implements Rajeev Gore's sequent calculus for S43.
 *)
 
-S43 = Modal0 +
+theory S43
+imports Modal0
+begin
 
 consts
   S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
@@ -15,17 +17,34 @@
   "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
                          ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
 
-rules
+ML {*
+  val S43pi  = "S43pi";
+  val SS43pi = "@S43pi";
+
+  val tr  = seq_tr;
+  val tr' = seq_tr';
+
+  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
+        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
+  fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
+        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
+
+*}
+
+parse_translation {* [(SS43pi,s43pi_tr)] *}
+print_translation {* [(S43pi,s43pi_tr')] *}
+
+axioms
 (* Definition of the star operation using a set of Horn clauses  *)
 (* For system S43: gamma * == {[]P | []P : gamma}                *)
 (*                 delta * == {<>P | <>P : delta}                *)
 
-  lstar0         "|L>"
-  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
-  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
-  rstar0         "|R>"
-  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
-  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
+  lstar0:         "|L>"
+  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
+  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
+  rstar0:         "|R>"
+  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
+  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
 
 (* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
 (* ie                                                                        *)
@@ -37,43 +56,27 @@
 (*    and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
 (*    and 1<=i<=k and k<j<=k+m                                               *)
 
-  S43pi0         "S43pi $L;; $R;; $Lbox; $Rdia"
-  S43pi1
-   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==> 
+  S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia"
+  S43pi1:
+   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==>
        S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
-  S43pi2
-   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==> 
+  S43pi2:
+   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==>
        S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
 
 (* Rules for [] and <> for S43 *)
 
-  boxL           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
-  diaR           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
-  pi1
-   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;  
-      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
+  boxL:           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
+  diaR:           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
+  pi1:
+   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;
+      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
    $L1, <>P, $L2 |- $R"
-  pi2
-   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;  
-      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
+  pi2:
+   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;
+      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
    $L |- $R1, []P, $R2"
-end
-
-ML
 
-local
-
-  val S43pi  = "S43pi";
-  val SS43pi = "@S43pi";
-
-  val tr  = Sequents.seq_tr;
-  val tr' = Sequents.seq_tr';
+ML {* use_legacy_bindings (the_context ()) *}
 
-  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
-        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
-  fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
-        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
-in
-val parse_translation = [(SS43pi,s43pi_tr)];
-val print_translation = [(S43pi,s43pi_tr')]
 end
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/Sequents.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,29 +1,29 @@
-(*  Title: 	Sequents/Sequents.thy
+(*  Title:      Sequents/Sequents.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
-
-Basis theory for parsing and pretty-printing of sequences to be used in
-Sequent Calculi. 
 *)
 
-Sequents = Pure +
+header {* Parsing and pretty-printing of sequences *}
+
+theory Sequents
+imports Pure
+uses ("prover.ML")
+begin
 
 global
 
-types
-  o 
-
+typedecl o
 
 (* Sequences *)
 
-types
+typedecl
  seq'
 
 consts
- SeqO'         :: [o,seq']=>seq'
- Seq1'         :: o=>seq'
-    
+ SeqO'         :: "[o,seq']=>seq'"
+ Seq1'         :: "o=>seq'"
+
 
 (* concrete syntax *)
 
@@ -32,37 +32,33 @@
 
 
 syntax
- SeqEmp         :: seq                                ("")
- SeqApp         :: [seqobj,seqcont] => seq            ("__")
+ SeqEmp         :: seq                                  ("")
+ SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
 
- SeqContEmp     :: seqcont                            ("")
- SeqContApp     :: [seqobj,seqcont] => seqcont        (",/ __")
-  
- SeqO           :: o => seqobj                        ("_")
- SeqId          :: 'a => seqobj                       ("$_")
+ SeqContEmp     :: seqcont                              ("")
+ SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
+
+ SeqO           :: "o => seqobj"                        ("_")
+ SeqId          :: "'a => seqobj"                       ("$_")
 
 types
-    
- single_seqe = [seq,seqobj] => prop
- single_seqi = [seq'=>seq',seq'=>seq'] => prop
- two_seqi    = [seq'=>seq', seq'=>seq'] => prop
- two_seqe    = [seq, seq] => prop
- three_seqi  = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
- three_seqe  = [seq, seq, seq] => prop
- four_seqi   = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
- four_seqe   = [seq, seq, seq, seq] => prop
+ single_seqe = "[seq,seqobj] => prop"
+ single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
+ two_seqi    = "[seq'=>seq', seq'=>seq'] => prop"
+ two_seqe    = "[seq, seq] => prop"
+ three_seqi  = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+ three_seqe  = "[seq, seq, seq] => prop"
+ four_seqi   = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+ four_seqe   = "[seq, seq, seq, seq] => prop"
 
-
- sequence_name = seq'=>seq'
+ sequence_name = "seq'=>seq'"
 
 
 syntax
   (*Constant to allow definitions of SEQUENCES of formulas*)
-  "@Side"        :: seq=>(seq'=>seq')     ("<<(_)>>")
+  "@Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
 
-end
-
-ML
+ML {*
 
 (* parse translation for sequences *)
 
@@ -70,49 +66,49 @@
 
 fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
     seqobj_tr(_ $ i) = i;
-    
+
 fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
-    seqcont_tr(Const("SeqContApp",_) $ so $ sc) = 
+    seqcont_tr(Const("SeqContApp",_) $ so $ sc) =
       (seqobj_tr so) $ (seqcont_tr sc);
 
 fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
-    seq_tr(Const("SeqApp",_) $ so $ sc) = 
+    seq_tr(Const("SeqApp",_) $ so $ sc) =
       abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
 
 
 fun singlobj_tr(Const("SeqO",_) $ f) =
     abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
-    
+
 
-    
+
 (* print translation for sequences *)
 
-fun seqcont_tr' (Bound 0) = 
+fun seqcont_tr' (Bound 0) =
       Const("SeqContEmp",dummyT) |
     seqcont_tr' (Const("SeqO'",_) $ f $ s) =
-      Const("SeqContApp",dummyT) $ 
-      (Const("SeqO",dummyT) $ f) $ 
+      Const("SeqContApp",dummyT) $
+      (Const("SeqO",dummyT) $ f) $
       (seqcont_tr' s) |
-(*    seqcont_tr' ((a as Abs(_,_,_)) $ s)= 
+(*    seqcont_tr' ((a as Abs(_,_,_)) $ s)=
       seqcont_tr'(betapply(a,s)) | *)
-    seqcont_tr' (i $ s) = 
-      Const("SeqContApp",dummyT) $ 
-      (Const("SeqId",dummyT) $ i) $ 
+    seqcont_tr' (i $ s) =
+      Const("SeqContApp",dummyT) $
+      (Const("SeqId",dummyT) $ i) $
       (seqcont_tr' s);
 
 fun seq_tr' s =
-    let fun seq_itr' (Bound 0) = 
+    let fun seq_itr' (Bound 0) =
               Const("SeqEmp",dummyT) |
             seq_itr' (Const("SeqO'",_) $ f $ s) =
-              Const("SeqApp",dummyT) $ 
+              Const("SeqApp",dummyT) $
               (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
 (*            seq_itr' ((a as Abs(_,_,_)) $ s) =
               seq_itr'(betapply(a,s)) |    *)
             seq_itr' (i $ s) =
-              Const("SeqApp",dummyT) $ 
-              (Const("SeqId",dummyT) $ i) $ 
+              Const("SeqApp",dummyT) $
+              (Const("SeqId",dummyT) $ i) $
               (seqcont_tr' s)
-    in case s of 
+    in case s of
          Abs(_,_,t) => seq_itr' t |
          _ => s $ (Bound 0)
     end;
@@ -138,22 +134,28 @@
 
 
 fun single_tr' c [s1, s2] =
-(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 ); 
+(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 );
 
 
 fun two_seq_tr' c [s1, s2] =
-  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 
+  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
 
 fun three_seq_tr' c [s1, s2, s3] =
-  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; 
+  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
 
 fun four_seq_tr' c [s1, s2, s3, s4] =
-  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; 
+  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
+
 
 
-			 
 (** for the <<...>> notation **)
-  
+
 fun side_tr [s1] = seq_tr s1;
+*}
 
-val parse_translation = [("@Side", side_tr)];
+parse_translation {* [("@Side", side_tr)] *}
+
+use "prover.ML"
+
+end
+
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/T.ML
--- a/src/Sequents/T.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/T.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -1,10 +1,10 @@
-(*  Title:      Modal/T
+(*  Title:      Modal/T.ML
     ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
 
-local open Modal0_rls T
+local open Modal0_rls
 in structure MP_Rule : MODAL_PROVER_RULE =
    struct
     val rewrite_rls = rewrite_rls
@@ -14,4 +14,4 @@
     val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
    end
 end;
-structure T_Prover = Modal_ProverFun(MP_Rule);  
+structure T_Prover = Modal_ProverFun(MP_Rule);
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/T.thy
--- a/src/Sequents/T.thy	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/T.thy	Sun Sep 18 15:20:08 2005 +0200
@@ -1,30 +1,36 @@
-(*  Title:      Modal/T
+(*  Title:      Modal/T.thy
     ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
 
-T = Modal0 +
-rules
+theory T
+imports Modal0
+begin
+
+axioms
 (* Definition of the star operation using a set of Horn clauses *)
 (* For system T:  gamma * == {P | []P : gamma}                  *)
 (*                delta * == {P | <>P : delta}                  *)
 
-  lstar0         "|L>"
-  lstar1         "$G |L> $H ==> []P, $G |L> P, $H"
-  lstar2         "$G |L> $H ==>   P, $G |L>    $H"
-  rstar0         "|R>"
-  rstar1         "$G |R> $H ==> <>P, $G |R> P, $H"
-  rstar2         "$G |R> $H ==>   P, $G |R>    $H"
+  lstar0:         "|L>"
+  lstar1:         "$G |L> $H ==> []P, $G |L> P, $H"
+  lstar2:         "$G |L> $H ==>   P, $G |L>    $H"
+  rstar0:         "|R>"
+  rstar1:         "$G |R> $H ==> <>P, $G |R> P, $H"
+  rstar2:         "$G |R> $H ==>   P, $G |R>    $H"
 
 (* Rules for [] and <> *)
 
-  boxR
-   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
+  boxR:
+   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
                $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
-  boxL     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
-  diaR     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
-  diaL
-   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
+  boxL:     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
+  diaR:     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
+  diaL:
+   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
                $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
diff -r fd19f77dcf60 -r 75166ebb619b src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/simpdata.ML	Sun Sep 18 15:20:08 2005 +0200
@@ -12,7 +12,7 @@
 
 fun prove_fun s =
  (writeln s;
-  prove_goal LK.thy s
+  prove_goal (the_context ()) s
    (fn prems => [ (cut_facts_tac prems 1),
                   (fast_tac (pack() add_safes [subst]) 1) ]));
 
@@ -144,7 +144,7 @@
 
 (*** Named rewrite rules ***)
 
-fun prove nm thm  = qed_goal nm LK.thy thm
+fun prove nm thm  = qed_goal nm (the_context ()) thm
     (fn prems => [ (cut_facts_tac prems 1),
                    (fast_tac LK_pack 1) ]);
 
@@ -264,7 +264,7 @@
 
 (* To create substition rules *)
 
-qed_goal "eq_imp_subst" LK.thy "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
+qed_goal "eq_imp_subst" (the_context ()) "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
   (fn prems =>
    [cut_facts_tac prems 1,
     asm_simp_tac LK_basic_ss 1]);