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/HOL/Word/WordArith.thy
changeset 28823 dcbef866c9e2
parent 28059 295a8fc92684
child 28959 9d35303719b5 
--- a/src/HOL/Word/WordArith.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Word/WordArith.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -19,9 +19,8 @@
            simp: word_uint.Rep_inject [symmetric])
 
 lemma signed_linorder: "linorder word_sle word_sless"
-  apply unfold_locales
-      apply (unfold word_sle_def word_sless_def) 
-  by auto 
+proof
+qed (unfold word_sle_def word_sless_def, auto)
 
 interpretation signed: linorder ["word_sle" "word_sless"] 
   by (rule signed_linorder)
isabelle