domain package:
* minor changes to some names and values (for consistency),
e.g. cases -> casedist, dists_eq -> dist_eqs,
[take_lemma] -> take_lemmas
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Thu Oct 30 14:17:33 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Thu Oct 30 14:18:14 1997 +0100
@@ -699,7 +699,7 @@
\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
by (strip_tac 1);
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (rtac mp 1);
by (assume_tac 2);
back();back();back();back();
@@ -941,7 +941,7 @@
\ --> Filter (%a. a:act B)`(mksch A B`tr`schA`schB) = schB";
by (strip_tac 1);
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (rtac mp 1);
by (assume_tac 2);
back();back();back();back();
--- a/src/HOLCF/IOA/meta_theory/Seq.ML Thu Oct 30 14:17:33 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML Thu Oct 30 14:18:14 1997 +0100
@@ -284,7 +284,7 @@
goal thy "!!x. x~=nil ==> szip`x`UU=UU";
by (stac szip_unfold 1);
by (Asm_full_simp_tac 1);
-by (res_inst_tac [("x","x")] seq.cases 1);
+by (res_inst_tac [("x","x")] seq.casedist 1);
by (REPEAT (Asm_full_simp_tac 1));
qed"szip_UU2";
@@ -324,7 +324,7 @@
qed"scons_inject_eq";
goal thy "!!x. nil<<x ==> nil=x";
-by (res_inst_tac [("x","x")] seq.cases 1);
+by (res_inst_tac [("x","x")] seq.casedist 1);
by (hyp_subst_tac 1);
by (etac antisym_less 1);
by (Asm_full_simp_tac 1);
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Oct 30 14:17:33 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Oct 30 14:18:14 1997 +0100
@@ -119,7 +119,7 @@
goal thy "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)";
by (simp_tac (!simpset addsimps [Last_def, Cons_def]) 1);
-by (res_inst_tac [("x","xs")] seq.cases 1);
+by (res_inst_tac [("x","xs")] seq.casedist 1);
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (REPEAT (Asm_simp_tac 1));
qed"Last_cons";
@@ -170,7 +170,7 @@
goal thy "!! x. x~=nil ==> Zip`x`UU =UU";
by (stac Zip_unfold 1);
by (Simp_tac 1);
-by (res_inst_tac [("x","x")] seq.cases 1);
+by (res_inst_tac [("x","x")] seq.casedist 1);
by (REPEAT (Asm_full_simp_tac 1));
qed"Zip_UU2";
@@ -884,7 +884,7 @@
goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
by (rtac iffI 1);
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (Auto_tac());
qed"seq_take_lemma";
@@ -972,7 +972,7 @@
\ ==> A x --> (f x)=(g x)";
by (case_tac "Forall Q x" 1);
by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (Auto_tac());
qed"take_lemma_principle2";
@@ -993,7 +993,7 @@
\ = seq_take (Suc n)`(g (s1 @@ y>>s2)) |] \
\ ==> A x --> (f x)=(g x)";
by (rtac impI 1);
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (rtac mp 1);
by (assume_tac 2);
by (res_inst_tac [("x","x")] spec 1);
@@ -1015,7 +1015,7 @@
\ = seq_take n`(g (s1 @@ y>>s2)) |] \
\ ==> A x --> (f x)=(g x)";
by (rtac impI 1);
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (rtac mp 1);
by (assume_tac 2);
by (res_inst_tac [("x","x")] spec 1);
@@ -1067,7 +1067,7 @@
\ = seq_take n`(g (s1 @@ y>>s2) h1 h2) |] \
\ ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)";
by (strip_tac 1);
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (rtac mp 1);
by (assume_tac 2);
by (res_inst_tac [("x","h2a")] spec 1);
@@ -1121,7 +1121,7 @@
\ = seq_take (Suc n)`(g (y>>s)) |] \
\ ==> A x --> (f x)=(g x)";
by (rtac impI 1);
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (rtac mp 1);
by (assume_tac 2);
by (res_inst_tac [("x","x")] spec 1);
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Thu Oct 30 14:17:33 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Thu Oct 30 14:18:14 1997 +0100
@@ -184,7 +184,7 @@
goal thy "Finite s --> (? y. s = Cut P s @@ y)";
by (strip_tac 1);
by (rtac exI 1);
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (rtac mp 1);
by (assume_tac 2);
by (thin_tac' 1 1);