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/Algebra/Module.thy
changeset 28823 dcbef866c9e2
parent 27714 27b4d7c01f8b
child 29237 e90d9d51106b 
--- a/src/HOL/Algebra/Module.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Module.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -91,11 +91,11 @@
 
 lemma (in algebra) R_cring:
   "cring R"
-  by unfold_locales
+  ..
 
 lemma (in algebra) M_cring:
   "cring M"
-  by unfold_locales
+  ..
 
 lemma (in algebra) module:
   "module R M"
isabelle