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.
changed 'code nofunc' to 'code func del'
authorhaftmann
Mon, 07 May 2007 09:58:07 +0200
changeset 22849 3c41e8492ba6
parent 22848 f65a76867179
child 22850 e795b5a031af
changed 'code nofunc' to 'code func del'
src/HOL/Library/MLString.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/MLString.thy	Mon May 07 00:52:25 2007 +0200
+++ b/src/HOL/Library/MLString.thy	Mon May 07 09:58:07 2007 +0200
@@ -26,7 +26,7 @@
 
 datatype ml_string = STR string
 
-lemmas [code nofunc] = ml_string.recs ml_string.cases
+lemmas [code func del] = ml_string.recs ml_string.cases
 
 lemma [code func]: "size (s\<Colon>ml_string) = 0"
   by (cases s) simp_all
isabelle