simpset extension moved from HOLCF.ML to One.ML and Tr2.ML
authorsandnerr
Mon Dec 09 19:13:13 1996 +0100 (1996-12-09)
changeset 2355ee9bdbe2ac8a
parent 2354 b4a1e3306aa0
child 2356 125260ef480c
simpset extension moved from HOLCF.ML to One.ML and Tr2.ML
src/HOLCF/HOLCF.ML
src/HOLCF/One.ML
src/HOLCF/Tr2.ML
     1.1 --- a/src/HOLCF/HOLCF.ML	Mon Dec 09 19:11:11 1996 +0100
     1.2 +++ b/src/HOLCF/HOLCF.ML	Mon Dec 09 19:13:13 1996 +0100
     1.3 @@ -6,7 +6,4 @@
     1.4  
     1.5  open HOLCF;
     1.6  
     1.7 -Addsimps (one_when @ dist_less_one @ dist_eq_one @ dist_less_tr @ dist_eq_tr
     1.8 -          @ tr_when @ andalso_thms @ orelse_thms @ neg_thms @ ifte_thms);
     1.9 -
    1.10  val HOLCF_ss = !simpset;
     2.1 --- a/src/HOLCF/One.ML	Mon Dec 09 19:11:11 1996 +0100
     2.2 +++ b/src/HOLCF/One.ML	Mon Dec 09 19:13:13 1996 +0100
     2.3 @@ -96,3 +96,4 @@
     2.4  
     2.5  val one_when = map prover ["one_when`x`UU = UU","one_when`x`one = x"];
     2.6  
     2.7 +Addsimps (one_when @ dist_less_one @ dist_eq_one);
     2.8 \ No newline at end of file
     3.1 --- a/src/HOLCF/Tr2.ML	Mon Dec 09 19:11:11 1996 +0100
     3.2 +++ b/src/HOLCF/Tr2.ML	Mon Dec 09 19:13:13 1996 +0100
     3.3 @@ -92,7 +92,8 @@
     3.4                          "If FF then e1 else e2 fi = e2",
     3.5                          "If TT then e1 else e2 fi = e1"];
     3.6  
     3.7 -
     3.8 +Addsimps (dist_less_tr @ dist_eq_tr @ tr_when @ andalso_thms @ 
     3.9 +	  orelse_thms @ neg_thms @ ifte_thms);
    3.10  
    3.11  
    3.12