# HG changeset patch
# User sandnerr
# Date 850155193 -3600
# Node ID ee9bdbe2ac8a3e23292218ba6992614b029f1f8d
# Parent  b4a1e3306aa0b253a50ad4c0215eda959bd7012f
simpset extension moved from HOLCF.ML to One.ML and Tr2.ML

diff -r b4a1e3306aa0 -r ee9bdbe2ac8a src/HOLCF/HOLCF.ML
--- a/src/HOLCF/HOLCF.ML	Mon Dec 09 19:11:11 1996 +0100
+++ b/src/HOLCF/HOLCF.ML	Mon Dec 09 19:13:13 1996 +0100
@@ -6,7 +6,4 @@
 
 open HOLCF;
 
-Addsimps (one_when @ dist_less_one @ dist_eq_one @ dist_less_tr @ dist_eq_tr
-          @ tr_when @ andalso_thms @ orelse_thms @ neg_thms @ ifte_thms);
-
 val HOLCF_ss = !simpset;
diff -r b4a1e3306aa0 -r ee9bdbe2ac8a src/HOLCF/One.ML
--- a/src/HOLCF/One.ML	Mon Dec 09 19:11:11 1996 +0100
+++ b/src/HOLCF/One.ML	Mon Dec 09 19:13:13 1996 +0100
@@ -96,3 +96,4 @@
 
 val one_when = map prover ["one_when`x`UU = UU","one_when`x`one = x"];
 
+Addsimps (one_when @ dist_less_one @ dist_eq_one);
\ No newline at end of file
diff -r b4a1e3306aa0 -r ee9bdbe2ac8a src/HOLCF/Tr2.ML
--- a/src/HOLCF/Tr2.ML	Mon Dec 09 19:11:11 1996 +0100
+++ b/src/HOLCF/Tr2.ML	Mon Dec 09 19:13:13 1996 +0100
@@ -92,7 +92,8 @@
                         "If FF then e1 else e2 fi = e2",
                         "If TT then e1 else e2 fi = e1"];
 
-
+Addsimps (dist_less_tr @ dist_eq_tr @ tr_when @ andalso_thms @ 
+	  orelse_thms @ neg_thms @ ifte_thms);