src/HOLCF/Tr2.ML
changeset 2355 ee9bdbe2ac8a
parent 1461 6bcb44e4d6e5
child 2453 2d416226b27d
--- 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);