# HG changeset patch
# User huffman
# Date 1118712915 -7200
# Node ID a9dec19693488ae4df4a600425eec55b70ada224
# Parent  90c51c932154a72755fe031d764fc3d4a5278b34
up_eq and up_less in default simpset now

diff -r 90c51c932154 -r a9dec1969348 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Mon Jun 13 21:28:57 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML	Tue Jun 14 03:35:15 2005 +0200
@@ -317,20 +317,18 @@
 val inverts =
   let
     val abs_less = ax_abs_iso RS (allI RS injection_less) RS iffD1;
-    val simps = [up_less, spair_less];
     val tacs = [
       dtac abs_less 1,
       REPEAT (dresolve_tac [sinl_less RS iffD1, sinr_less RS iffD1] 1),
-      asm_full_simp_tac (HOLCF_ss addsimps simps) 1];
+      asm_full_simp_tac (HOLCF_ss addsimps [spair_less]) 1];
   in map (fn (con,args) => pgterm (op <<) con args tacs) cons' end;
 val injects =
   let
     val abs_eq = ax_abs_iso RS (allI RS injection_eq) RS iffD1;
-    val simps = [up_eq, spair_eq];
     val tacs = [
       dtac abs_eq 1,
       REPEAT (dresolve_tac [sinl_inject, sinr_inject] 1),
-      asm_full_simp_tac (HOLCF_ss addsimps simps) 1];
+      asm_full_simp_tac (HOLCF_ss addsimps [spair_eq]) 1];
   in map (fn (con,args) => pgterm (op ===) con args tacs) cons' end;
 end;