converted legacy ML scripts;
authorwenzelm
Tue Nov 21 00:00:39 2006 +0100 (2006-11-21)
changeset 214277c8f4a331f9b
parent 21426 87ac12bed1ab
child 21428 f84cf8e9cad8
converted legacy ML scripts;
src/Sequents/ILL.ML
src/Sequents/ILL.thy
src/Sequents/ILL_predlog.thy
src/Sequents/IsaMakefile
     1.1 --- a/src/Sequents/ILL.ML	Mon Nov 20 23:47:10 2006 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,168 +0,0 @@
     1.4 -(*  Title:      Sequents/ILL.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Sara Kalvala and Valeria de Paiva
     1.7 -    Copyright   1992  University of Cambridge
     1.8 -*)
     1.9 -
    1.10 -val lazy_cs = empty_pack
    1.11 - add_safes [tensl, conjr, disjl, promote0,
    1.12 -            context2,context3]
    1.13 - add_unsafes [identity, zerol, conjll, conjlr, disjrl, disjrr,
    1.14 -               impr, tensr, impl, derelict, weaken,
    1.15 -                 promote1, promote2,context1,context4a,context4b];
    1.16 -
    1.17 -fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n);
    1.18 -
    1.19 -fun auto x = prove_goal (the_context ()) x (fn prems => [best_tac lazy_cs 1]);
    1.20 -
    1.21 -Goal "$F, $G |- A ==> $F, !(A -o B), $G |- B";
    1.22 -by (rtac derelict 1);
    1.23 -by (rtac impl 1);
    1.24 -by (rtac identity 2);
    1.25 -by (rtac context1 1);
    1.26 -by (assume_tac 1);
    1.27 -qed "aux_impl";
    1.28 -
    1.29 -Goal " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C";
    1.30 -by (rtac contract 1);
    1.31 -by (res_inst_tac [("A","(!A) >< (!B)")] cut 1);
    1.32 -by (rtac tensr 2);
    1.33 -by (rtac (auto "! (A && B) |- !A") 3);
    1.34 -by (rtac (auto "! (A && B) |- !B") 3);
    1.35 -by (rtac context1 2);
    1.36 -by (rtac tensl 2);
    1.37 -by (assume_tac 2);
    1.38 -by (rtac context3 1);
    1.39 -by (rtac context3 1);
    1.40 -by (rtac context1 1);
    1.41 -qed "conj_lemma";
    1.42 -
    1.43 -Goal "!A, !A, $G |- B ==> $G |- (!A) -o B";
    1.44 -by (rtac impr 1);
    1.45 -by (rtac contract 1);
    1.46 -by (assume_tac 1);
    1.47 -qed "impr_contract";
    1.48 -
    1.49 -
    1.50 -Goal "A, !A, $G |- B ==> $G |- (!A) -o B";
    1.51 -by (rtac impr 1);
    1.52 -by (rtac contract 1);
    1.53 -by (rtac derelict 1);
    1.54 -by (assume_tac 1);
    1.55 -qed "impr_contr_der";
    1.56 -
    1.57 -val _ = goal (the_context ()) "$F, (!B) -o 0, $G, !B, $H |- A";
    1.58 -by (rtac impl 1);
    1.59 -by (rtac identity 3);
    1.60 -by (rtac context3 1);
    1.61 -by (rtac context1 1);
    1.62 -by (rtac zerol 1);
    1.63 -qed "contrad1";
    1.64 -
    1.65 -
    1.66 -val _ = goal (the_context ()) "$F, !B, $G, (!B) -o 0, $H |- A";
    1.67 -by (rtac impl 1);
    1.68 -by (rtac identity 3);
    1.69 -by (rtac context3 1);
    1.70 -by (rtac context1 1);
    1.71 -by (rtac zerol 1);
    1.72 -qed "contrad2";
    1.73 -
    1.74 -val _ = goal (the_context ()) "A -o B, A |- B";
    1.75 -by (rtac impl 1);
    1.76 -by (rtac identity 2);
    1.77 -by (rtac identity 2);
    1.78 -by (rtac context1 1);
    1.79 -qed "ll_mp";
    1.80 -
    1.81 -Goal "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C";
    1.82 -by (res_inst_tac [("A","B")] cut 1);
    1.83 -by (rtac ll_mp 2);
    1.84 -by (assume_tac 2);
    1.85 -by (rtac context3 1);
    1.86 -by (rtac context3 1);
    1.87 -by (rtac context1 1);
    1.88 -qed "mp_rule1";
    1.89 -
    1.90 -Goal "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C";
    1.91 -by (res_inst_tac [("A","B")] cut 1);
    1.92 -by (rtac ll_mp 2);
    1.93 -by (assume_tac 2);
    1.94 -by (rtac context3 1);
    1.95 -by (rtac context3 1);
    1.96 -by (rtac context1 1);
    1.97 -qed "mp_rule2";
    1.98 -
    1.99 -val _ = goal (the_context ()) "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
   1.100 -by (best_tac lazy_cs 1);
   1.101 -qed "or_to_and";
   1.102 -
   1.103 -Goal "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \
   1.104 -\         $F, !((!(A ++ B)) -o 0), $G |- C";
   1.105 -by (rtac cut 1);
   1.106 -by (rtac or_to_and 2);
   1.107 -by (assume_tac 2);
   1.108 -by (rtac context3 1);
   1.109 -by (rtac context1 1);
   1.110 -qed "o_a_rule";
   1.111 -
   1.112 -
   1.113 -
   1.114 -val _ = goal (the_context ()) "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
   1.115 -by (rtac impr 1);
   1.116 -by (rtac conj_lemma 1);
   1.117 -by (rtac disjl 1);
   1.118 -by (ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs));
   1.119 -qed "conj_imp";
   1.120 -
   1.121 -
   1.122 -val not_imp = auto "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0";
   1.123 -
   1.124 -Goal "!A -o (!A -o 0) |- !A -o 0";
   1.125 -by (rtac impr 1);
   1.126 -by (rtac contract 1);
   1.127 -by (rtac impl 1);
   1.128 -by (rtac identity 3);
   1.129 -by (rtac context1 1);
   1.130 -by (best_tac lazy_cs 1);
   1.131 -qed "a_not_a";
   1.132 -
   1.133 -Goal "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B";
   1.134 -by (res_inst_tac [("A","!A -o 0")] cut 1);
   1.135 -by (rtac a_not_a 2);
   1.136 -by (assume_tac 2);
   1.137 -by (best_tac lazy_cs 1);
   1.138 -qed "a_not_a_rule";
   1.139 -
   1.140 -fun thm_to_rule x y =
   1.141 -    prove_goal (the_context ()) x
   1.142 -      (fn [prem] => [(rtac cut 1), (rtac y 2), (rtac prem 2),
   1.143 -                     (best_tac lazy_cs 1)]);
   1.144 -
   1.145 -val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1,
   1.146 -                                 contrad2, mp_rule1, mp_rule2, o_a_rule,
   1.147 -                                 a_not_a_rule]
   1.148 -                      add_unsafes [aux_impl];
   1.149 -
   1.150 -val power_cs = safe_cs add_unsafes [impr_contr_der];
   1.151 -
   1.152 -fun auto1 x = prove_goal (the_context ()) x (fn prems => [best_tac safe_cs 1]) ;
   1.153 -
   1.154 -fun auto2 x = prove_goal (the_context ()) x (fn prems => [best_tac power_cs 1]) ;
   1.155 -
   1.156 -
   1.157 -(* some examples from Troelstra and van Dalen
   1.158 -
   1.159 -auto1  "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0";
   1.160 -
   1.161 -auto1  "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))";
   1.162 -
   1.163 -auto1  "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |- \
   1.164 -\        (!A) -o ( (!  ((!B) -o 0)) -o 0)";
   1.165 -
   1.166 -
   1.167 -auto2  "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |- \
   1.168 -\         (!((! ((!A) -o B) ) -o 0)) -o 0";
   1.169 -
   1.170 -
   1.171 -                                                         *)
     2.1 --- a/src/Sequents/ILL.thy	Mon Nov 20 23:47:10 2006 +0100
     2.2 +++ b/src/Sequents/ILL.thy	Tue Nov 21 00:00:39 2006 +0100
     2.3 @@ -123,6 +123,185 @@
     2.4  context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
     2.5  context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
     2.6  
     2.7 -ML {* use_legacy_bindings (the_context ()) *}
     2.8 +
     2.9 +ML {*
    2.10 +
    2.11 +val lazy_cs = empty_pack
    2.12 +  add_safes [thm "tensl", thm "conjr", thm "disjl", thm "promote0",
    2.13 +    thm "context2", thm "context3"]
    2.14 +  add_unsafes [thm "identity", thm "zerol", thm "conjll", thm "conjlr",
    2.15 +    thm "disjrl", thm "disjrr", thm "impr", thm "tensr", thm "impl",
    2.16 +    thm "derelict", thm "weaken", thm "promote1", thm "promote2",
    2.17 +    thm "context1", thm "context4a", thm "context4b"];
    2.18 +
    2.19 +local
    2.20 +  val promote0 = thm "promote0"
    2.21 +  val promote1 = thm "promote1"
    2.22 +  val promote2 = thm "promote2"
    2.23 +in
    2.24 +
    2.25 +fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n)
    2.26  
    2.27  end
    2.28 +*}
    2.29 +
    2.30 +method_setup best_lazy =
    2.31 +{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac lazy_cs)) *}
    2.32 +"lazy classical reasoning"
    2.33 +
    2.34 +lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
    2.35 +  apply (rule derelict)
    2.36 +  apply (rule impl)
    2.37 +  apply (rule_tac [2] identity)
    2.38 +  apply (rule context1)
    2.39 +  apply assumption
    2.40 +  done
    2.41 +
    2.42 +lemma conj_lemma: " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
    2.43 +  apply (rule contract)
    2.44 +  apply (rule_tac A = " (!A) >< (!B) " in cut)
    2.45 +  apply (rule_tac [2] tensr)
    2.46 +  prefer 3
    2.47 +  apply (subgoal_tac "! (A && B) |- !A")
    2.48 +  apply assumption
    2.49 +  apply best_lazy
    2.50 +  prefer 3
    2.51 +  apply (subgoal_tac "! (A && B) |- !B")
    2.52 +  apply assumption
    2.53 +  apply best_lazy
    2.54 +  apply (rule_tac [2] context1)
    2.55 +  apply (rule_tac [2] tensl)
    2.56 +  prefer 2 apply (assumption)
    2.57 +  apply (rule context3)
    2.58 +  apply (rule context3)
    2.59 +  apply (rule context1)
    2.60 +  done
    2.61 +
    2.62 +lemma impr_contract: "!A, !A, $G |- B ==> $G |- (!A) -o B"
    2.63 +  apply (rule impr)
    2.64 +  apply (rule contract)
    2.65 +  apply assumption
    2.66 +  done
    2.67 +
    2.68 +lemma impr_contr_der: "A, !A, $G |- B ==> $G |- (!A) -o B"
    2.69 +  apply (rule impr)
    2.70 +  apply (rule contract)
    2.71 +  apply (rule derelict)
    2.72 +  apply assumption
    2.73 +  done
    2.74 +
    2.75 +lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A"
    2.76 +  apply (rule impl)
    2.77 +  apply (rule_tac [3] identity)
    2.78 +  apply (rule context3)
    2.79 +  apply (rule context1)
    2.80 +  apply (rule zerol)
    2.81 +  done
    2.82 +
    2.83 +
    2.84 +lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A"
    2.85 +  apply (rule impl)
    2.86 +  apply (rule_tac [3] identity)
    2.87 +  apply (rule context3)
    2.88 +  apply (rule context1)
    2.89 +  apply (rule zerol)
    2.90 +  done
    2.91 +
    2.92 +lemma ll_mp: "A -o B, A |- B"
    2.93 +  apply (rule impl)
    2.94 +  apply (rule_tac [2] identity)
    2.95 +  apply (rule_tac [2] identity)
    2.96 +  apply (rule context1)
    2.97 +  done
    2.98 +
    2.99 +lemma mp_rule1: "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
   2.100 +  apply (rule_tac A = "B" in cut)
   2.101 +  apply (rule_tac [2] ll_mp)
   2.102 +  prefer 2 apply (assumption)
   2.103 +  apply (rule context3)
   2.104 +  apply (rule context3)
   2.105 +  apply (rule context1)
   2.106 +  done
   2.107 +
   2.108 +lemma mp_rule2: "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
   2.109 +  apply (rule_tac A = "B" in cut)
   2.110 +  apply (rule_tac [2] ll_mp)
   2.111 +  prefer 2 apply (assumption)
   2.112 +  apply (rule context3)
   2.113 +  apply (rule context3)
   2.114 +  apply (rule context1)
   2.115 +  done
   2.116 +
   2.117 +lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
   2.118 +  by best_lazy
   2.119 +
   2.120 +lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==>  
   2.121 +          $F, !((!(A ++ B)) -o 0), $G |- C"
   2.122 +  apply (rule cut)
   2.123 +  apply (rule_tac [2] or_to_and)
   2.124 +  prefer 2 apply (assumption)
   2.125 +  apply (rule context3)
   2.126 +  apply (rule context1)
   2.127 +  done
   2.128 +
   2.129 +lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
   2.130 +  apply (rule impr)
   2.131 +  apply (rule conj_lemma)
   2.132 +  apply (rule disjl)
   2.133 +  apply (rule mp_rule1, best_lazy)+
   2.134 +  done
   2.135 +
   2.136 +lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"
   2.137 +  by best_lazy
   2.138 +
   2.139 +lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"
   2.140 +  apply (rule impr)
   2.141 +  apply (rule contract)
   2.142 +  apply (rule impl)
   2.143 +  apply (rule_tac [3] identity)
   2.144 +  apply (rule context1)
   2.145 +  apply best_lazy
   2.146 +  done
   2.147 +
   2.148 +lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
   2.149 +  apply (rule_tac A = "!A -o 0" in cut)
   2.150 +  apply (rule_tac [2] a_not_a)
   2.151 +  prefer 2 apply (assumption)
   2.152 +  apply best_lazy
   2.153 +  done
   2.154 +
   2.155 +ML {*
   2.156 +
   2.157 +val safe_cs = lazy_cs add_safes [thm "conj_lemma", thm "ll_mp", thm "contrad1",
   2.158 +                                 thm "contrad2", thm "mp_rule1", thm "mp_rule2", thm "o_a_rule",
   2.159 +                                 thm "a_not_a_rule"]
   2.160 +                      add_unsafes [thm "aux_impl"];
   2.161 +
   2.162 +val power_cs = safe_cs add_unsafes [thm "impr_contr_der"];
   2.163 +*}
   2.164 +
   2.165 +
   2.166 +method_setup best_safe =
   2.167 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} ""
   2.168 +
   2.169 +method_setup best_power =
   2.170 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} ""
   2.171 +
   2.172 +
   2.173 +(* Some examples from Troelstra and van Dalen *)
   2.174 +
   2.175 +lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"
   2.176 +  by best_safe
   2.177 +
   2.178 +lemma "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))"
   2.179 +  by best_safe
   2.180 +
   2.181 +lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |-
   2.182 +        (!A) -o ( (!  ((!B) -o 0)) -o 0)"
   2.183 +  by best_safe
   2.184 +
   2.185 +lemma "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |-
   2.186 +          (!((! ((!A) -o B) ) -o 0)) -o 0"
   2.187 +  by best_power
   2.188 +
   2.189 +end
     3.1 --- a/src/Sequents/ILL_predlog.thy	Mon Nov 20 23:47:10 2006 +0100
     3.2 +++ b/src/Sequents/ILL_predlog.thy	Tue Nov 21 00:00:39 2006 +0100
     3.3 @@ -29,107 +29,102 @@
     3.4  (* another translations for linear implication:
     3.5    "[* A > B *]" == "!([*A*] -o [*B*])" *)
     3.6  
     3.7 -method_setup auto1 =
     3.8 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} ""
     3.9 -method_setup auto2 =
    3.10 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} ""
    3.11 -
    3.12  (* from [kleene 52] pp 118,119 *)
    3.13  
    3.14  lemma k49a: "|- [* A > ( - ( - A)) *]"
    3.15 -  by auto1
    3.16 +  by best_safe
    3.17  
    3.18  lemma k49b: "|- [*( - ( - ( - A))) = ( - A)*]"
    3.19 -  by auto1
    3.20 +  by best_safe
    3.21  
    3.22  lemma k49c: "|- [* (A | - A) > ( - - A = A) *]"
    3.23 -  by auto1
    3.24 +  by best_safe
    3.25  
    3.26  lemma k50a: "|- [* - (A = - A) *]"
    3.27 -  by auto2
    3.28 +  by best_power
    3.29  
    3.30  lemma k51a: "|- [* - - (A | - A) *]"
    3.31 -  by auto1
    3.32 +  by best_safe
    3.33  
    3.34  lemma k51b: "|- [* - - (- - A > A) *]"
    3.35 -  by auto2
    3.36 +  by best_power
    3.37  
    3.38  lemma k56a: "|- [* (A | B) > - (- A & - B) *]"
    3.39 -  by auto1
    3.40 +  by best_safe
    3.41  
    3.42  lemma k56b: "|- [* (-A | B) > - (A & -B) *]"
    3.43 -  by auto1
    3.44 +  by best_safe
    3.45  
    3.46  lemma k57a: "|- [* (A & B) > - (-A | -B) *]"
    3.47 -  by auto1
    3.48 +  by best_safe
    3.49  
    3.50  lemma k57b: "|- [* (A & -B) > -(-A | B) *]"
    3.51 -  by auto2
    3.52 +  by best_power
    3.53  
    3.54  lemma k58a: "|- [* (A > B) > - (A & -B) *]"
    3.55 -  by auto1
    3.56 +  by best_safe
    3.57  
    3.58  lemma k58b: "|- [* (A > -B) = -(A & B) *]"
    3.59 -  by auto1
    3.60 +  by best_safe
    3.61  
    3.62  lemma k58c: "|- [* - (A & B) = (- - A > - B) *]"
    3.63 -  by auto1
    3.64 +  by best_safe
    3.65  
    3.66  lemma k58d: "|- [* (- - A > - B) = - - (-A | -B) *]"
    3.67 -  by auto1
    3.68 +  by best_safe
    3.69  
    3.70  lemma k58e: "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]"
    3.71 -  by auto1
    3.72 +  by best_safe
    3.73  
    3.74  lemma k58f: "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]"
    3.75 -  by auto1
    3.76 +  by best_safe
    3.77  
    3.78  lemma k58g: "|- [* (- -A > B) > - (A & -B) *]"
    3.79 -  by auto1
    3.80 +  by best_safe
    3.81  
    3.82  lemma k59a: "|- [* (-A | B) > (A > B) *]"
    3.83 -  by auto1
    3.84 +  by best_safe
    3.85  
    3.86  lemma k59b: "|- [* (A > B) > - - (-A | B) *]"
    3.87 -  by auto2
    3.88 +  by best_power
    3.89  
    3.90  lemma k59c: "|- [* (-A > B) > - -(A | B) *]"
    3.91 -  by auto2
    3.92 +  by best_power
    3.93  
    3.94  lemma k60a: "|- [* (A & B) > - (A > -B) *]"
    3.95 -  by auto1
    3.96 +  by best_safe
    3.97  
    3.98  lemma k60b: "|- [* (A & -B) > - (A > B) *]"
    3.99 -  by auto1
   3.100 +  by best_safe
   3.101  
   3.102  lemma k60c: "|- [* ( - - A & B) > - (A > -B) *]"
   3.103 -  by auto1
   3.104 +  by best_safe
   3.105  
   3.106  lemma k60d: "|- [* (- - A & - B) = - (A > B) *]"
   3.107 -  by auto1
   3.108 +  by best_safe
   3.109  
   3.110  lemma k60e: "|- [* - (A > B) = - (-A | B) *]"
   3.111 -  by auto1
   3.112 +  by best_safe
   3.113  
   3.114  lemma k60f: "|- [* - (-A | B) = - - (A & -B) *]"
   3.115 -  by auto1
   3.116 +  by best_safe
   3.117  
   3.118  lemma k60g: "|- [* - - (A > B) = - (A & -B) *]"
   3.119 -  by auto2
   3.120 +  by best_power
   3.121  
   3.122  lemma k60h: "|- [* - (A & -B) = (A > - -B) *]"
   3.123 -  by auto1
   3.124 +  by best_safe
   3.125  
   3.126  lemma k60i: "|- [* (A > - -B) = (- -A > - -B) *]"
   3.127 -  by auto1
   3.128 +  by best_safe
   3.129  
   3.130  lemma k61a: "|- [* (A | B) > (-A > B) *]"
   3.131 -  by auto1
   3.132 +  by best_safe
   3.133  
   3.134  lemma k61b: "|- [* - (A | B) = - (-A > B) *]"
   3.135 -  by auto2
   3.136 +  by best_power
   3.137  
   3.138  lemma k62a: "|- [* (-A | -B) > - (A & B) *]"
   3.139 -  by auto1
   3.140 +  by best_safe
   3.141  
   3.142  end
     4.1 --- a/src/Sequents/IsaMakefile	Mon Nov 20 23:47:10 2006 +0100
     4.2 +++ b/src/Sequents/IsaMakefile	Tue Nov 21 00:00:39 2006 +0100
     4.3 @@ -26,7 +26,7 @@
     4.4  Pure:
     4.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     4.6  
     4.7 -$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK0.thy LK.thy \
     4.8 +$(OUT)/Sequents: $(OUT)/Pure ILL.thy LK0.thy LK.thy \
     4.9    modal.ML ROOT.ML simpdata.ML S4.thy S43.thy Sequents.thy T.thy prover.ML \
    4.10    ILL_predlog.thy Washing.thy
    4.11  	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents