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";