# HG changeset patch
# User oheimb
# Date 878217557 -3600
# Node ID fdfef2d484caa3443410a7bb183c6010524d1b99
# Parent  35766855f344cb8b56357331357c7a3b3321bfd7
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 35766855f344 -r fdfef2d484ca src/HOLCF/ex/Dagstuhl.ML
--- 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);
diff -r 35766855f344 -r fdfef2d484ca src/HOLCF/ex/Dnat.ML
--- 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),
diff -r 35766855f344 -r fdfef2d484ca src/HOLCF/ex/Stream.ML
--- 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]);