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/ex/Loop.ML
changeset 4098 71e05eb27fb6
parent 3842 b55686a7b22c
child 9169 85a47aa21f74 
--- a/src/HOLCF/ex/Loop.ML	Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/ex/Loop.ML	Mon Nov 03 14:06:27 1997 +0100
@@ -119,7 +119,7 @@
         (nat_ind_tac "k" 1),
         (Asm_simp_tac 1),
         (strip_tac 1),
-        (simp_tac (!simpset addsimps [step_def2]) 1),
+        (simp_tac (simpset() addsimps [step_def2]) 1),
         (res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1),
         (etac notE 1),
         (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
isabelle