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.
Mod due to: Added a few thms about UN/INT/{}/UNIV
authornipkow
Fri, 18 Oct 2002 09:53:18 +0200
changeset 13654 b0d8bad27f42
parent 13653 ef123b9e8089
child 13655 95b95cdb4704
Mod due to: Added a few thms about UN/INT/{}/UNIV
src/HOL/Algebra/abstract/Ideal.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Algebra/abstract/Ideal.ML	Fri Oct 18 09:53:02 2002 +0200
+++ b/src/HOL/Algebra/abstract/Ideal.ML	Fri Oct 18 09:53:18 2002 +0200
@@ -74,7 +74,7 @@
 qed "generator_in_ideal";
 
 Goalw [ideal_of_def] "ideal_of {<1>::'a::ring} = UNIV";
-by (auto_tac (claset() addSDs [is_ideal_mult], simpset()));
+by (force_tac (claset() addDs [is_ideal_mult], simpset()) 1);
   (* loops if is_ideal_mult is added as non-safe rule *)
 qed "ideal_of_one_eq";
isabelle