fixed some abuses of addDs and addEs
authorpaulson
Wed, 28 Jun 2000 10:52:02 +0200
changeset 9168 77658111e122
parent 9167 5b6b65c90eeb
child 9169 85a47aa21f74
fixed some abuses of addDs and addEs
src/HOL/TLA/TLA.ML
--- a/src/HOL/TLA/TLA.ML	Wed Jun 28 10:50:27 2000 +0200
+++ b/src/HOL/TLA/TLA.ML	Wed Jun 28 10:52:02 2000 +0200
@@ -946,7 +946,7 @@
             Force_tac 1,
             etac STL4E 1,
             rtac DmdImpl 1,
-            force_tac (temp_css addSEs2 [prem RS wf_irrefl]) 1
+            force_tac (temp_css addIs2 [prem RS wf_irrefl]) 1
            ]);
 
 (* In particular, for natural numbers, if n decreases infinitely often
@@ -972,8 +972,8 @@
 
 qed_goal "aallI" TLA.thy 
   "[| basevars vs; (!!x. basevars (x,vs) ==> sigma |= F x) |] ==> sigma |= (AALL x. F x)"
-  (fn prems => [auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] 
-                                   addSIs2 prems addSDs2 prems)]);
+  (fn [prem1,prem2] => [auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] 
+                                   addSIs2 [prem1] addSDs2 [prem2])]);
 
 qed_goalw "aallE" TLA.thy [aall_def] "|- (AALL x. F x) --> F x"
    (K [Clarsimp_tac 1, etac swap 1,