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/ex/Numeral.thy
changeset 28823 dcbef866c9e2
parent 28562 4e74209f113e
child 29667 53103fc8ffa3 
--- a/src/HOL/ex/Numeral.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/ex/Numeral.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -699,7 +699,7 @@
 begin
 
 subclass semiring_1_minus
-  by unfold_locales (simp_all add: ring_simps)
+  proof qed (simp_all add: ring_simps)
 
 lemma Dig_zero_minus_of_num [numeral]:
   "0 - of_num n = - of_num n"
isabelle