Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Cprod2.ML
changeset 4098 71e05eb27fb6
parent 3842 b55686a7b22c
child 4721 c8a8482a8124 
--- a/src/HOLCF/Cprod2.ML	Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Cprod2.ML	Mon Nov 03 14:06:27 1997 +0100
@@ -40,7 +40,7 @@
 qed_goal "minimal_cprod" thy  "(UU,UU)<<p"
 (fn prems =>
         [
-        (simp_tac(!simpset addsimps[inst_cprod_po])1)
+        (simp_tac(simpset() addsimps[inst_cprod_po])1)
         ]);
 
 bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym);
@@ -62,13 +62,13 @@
         (strip_tac 1),
         (rtac (less_fun RS iffD2) 1),
         (strip_tac 1),
-        (asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
+        (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1)
         ]);
 
 qed_goalw "monofun_pair2" thy [monofun] "monofun(Pair x)"
  (fn prems =>
         [
-        (asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
+        (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1)
         ]);
 
 qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
isabelle