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.
unfold_locales workaround
authorballarin
Mon, 01 Oct 2007 12:24:45 +0200
changeset 24788 f0dba1cda0b5
parent 24787 df56433cc059
child 24789 33b7fbc07361
unfold_locales workaround
src/FOL/ex/LocaleTest.thy file | annotate | diff | comparison | revisions 
--- a/src/FOL/ex/LocaleTest.thy	Mon Oct 01 12:24:07 2007 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Mon Oct 01 12:24:45 2007 +0200
@@ -209,6 +209,7 @@
   interpret i9: ID [a beta _]
     apply - apply assumption
     apply unfold_locales
+    apply (rule refl) (*FIXME: should have been discharged by unfold_locales*)
     apply (rule refl) done
 qed rule
isabelle