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.
imports Commutative_Ring instead of Main, since the latter hides our names;
authorwenzelm
Wed, 14 Sep 2005 23:14:59 +0200
changeset 17396 1ca607b28670
parent 17395 a05e20f6a31a
child 17397 4ef3da248c48
imports Commutative_Ring instead of Main, since the latter hides our names;
src/HOL/ex/Commutative_Ring_Complete.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Sep 14 23:14:58 2005 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Sep 14 23:14:59 2005 +0200
@@ -9,7 +9,7 @@
 header {* Proof of the relative completeness of method comm-ring *}
 
 theory Commutative_Ring_Complete
-imports Main
+imports Commutative_Ring  (*do not use Main here, since it hides our consts*)
 begin
 	
   (* Fromalization of normal form *)
isabelle