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.
imp_conv_disj is now declared as a "code unfold" lemma to avoid that
authorberghofe
Tue, 08 Jan 2008 10:24:34 +0100
changeset 25860 844ab7ace3db
parent 25859 9bc18bf8be2d
child 25861 494d9301cc75
imp_conv_disj is now declared as a "code unfold" lemma to avoid that conclusion is evaluated eagerly.
src/HOL/Code_Setup.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Code_Setup.thy	Mon Jan 07 11:40:20 2008 +0100
+++ b/src/HOL/Code_Setup.thy	Tue Jan 08 10:24:34 2008 +0100
@@ -84,7 +84,7 @@
 
 text {* type bool *}
 
-lemmas [code] = imp_conv_disj
+lemmas [code unfold] = imp_conv_disj
 
 code_type bool
   (SML "bool")
isabelle