# HG changeset patch
# User oheimb
# Date 878217494 -3600
# Node ID 8abc33930ff01adf3bceb583570d147fee58f423
# Parent  4df7f385fe9faaeac50a99588a2d65753a9cd7f7
domain package:
* minor changes to some names and values (for consistency),
    e.g. cases -> casedist, dists_eq -> dist_eqs,
	 [take_lemma] -> take_lemmas

diff -r 4df7f385fe9f -r 8abc33930ff0 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- 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();
diff -r 4df7f385fe9f -r 8abc33930ff0 src/HOLCF/IOA/meta_theory/Seq.ML
--- 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);
diff -r 4df7f385fe9f -r 8abc33930ff0 src/HOLCF/IOA/meta_theory/Sequence.ML
--- 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);
diff -r 4df7f385fe9f -r 8abc33930ff0 src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- 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);