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/ex/Dagstuhl.ML Thu Oct 30 14:19:01 1997 +0100
+++ b/src/HOLCF/ex/Dagstuhl.ML Thu Oct 30 14:19:17 1997 +0100
@@ -32,7 +32,7 @@
val lemma5=result();
val prems = goal Dagstuhl.thy "YS = YYS";
-by (rtac stream.take_lemma 1);
+by (resolve_tac stream.take_lemmas 1);
by (nat_ind_tac "n" 1);
by (simp_tac (!simpset addsimps stream.rews) 1);
by (stac YS_def2 1);
--- a/src/HOLCF/ex/Dnat.ML Thu Oct 30 14:19:01 1997 +0100
+++ b/src/HOLCF/ex/Dnat.ML Thu Oct 30 14:19:17 1997 +0100
@@ -53,14 +53,14 @@
(res_inst_tac [("x","x")] dnat.ind 1),
(fast_tac HOL_cs 1),
(rtac allI 1),
- (res_inst_tac [("x","y")] dnat.cases 1),
+ (res_inst_tac [("x","y")] dnat.casedist 1),
(fast_tac (HOL_cs addSIs [UU_I]) 1),
(Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dnat.dists_le) 1),
+ (asm_simp_tac (!simpset addsimps dnat.dist_les) 1),
(rtac allI 1),
- (res_inst_tac [("x","y")] dnat.cases 1),
+ (res_inst_tac [("x","y")] dnat.casedist 1),
(fast_tac (HOL_cs addSIs [UU_I]) 1),
- (asm_simp_tac (!simpset addsimps dnat.dists_le) 1),
+ (asm_simp_tac (!simpset addsimps dnat.dist_les) 1),
(asm_simp_tac (!simpset addsimps dnat.rews) 1),
(strip_tac 1),
(subgoal_tac "d<<da" 1),
--- a/src/HOLCF/ex/Stream.ML Thu Oct 30 14:19:01 1997 +0100
+++ b/src/HOLCF/ex/Stream.ML Thu Oct 30 14:19:17 1997 +0100
@@ -8,7 +8,7 @@
open Stream;
-fun stream_case_tac s i = res_inst_tac [("x",s)] stream.cases i
+fun stream_case_tac s i = res_inst_tac [("x",s)] stream.casedist i
THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
@@ -244,7 +244,7 @@
rtac allI 1,
stream_case_tac "s" 1,
asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1,
- res_inst_tac [("x","sa")] stream.cases 1,
+ res_inst_tac [("x","sa")] stream.casedist 1,
asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1,
asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1]);