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