Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix looping simplifier
authorhuffman
Fri, 16 May 2008 21:41:07 +0200
changeset 26921 5d9f78c3d6de
parent 26920 7f5b390a4448
child 26922 c795d4b706b1
fix looping simplifier
src/HOLCF/SetPcpo.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/SetPcpo.thy	Thu May 15 22:57:54 2008 +0200
+++ b/src/HOLCF/SetPcpo.thy	Fri May 16 21:41:07 2008 +0200
@@ -16,7 +16,7 @@
   less_bool_def: "(op \<sqsubseteq>) = (op \<longrightarrow>)"
 
 instance
-by (intro_classes, auto simp add: less_bool_def)
+by (intro_classes, unfold less_bool_def, safe)
 
 end
isabelle