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/Ideal.thy
changeset 27714 27b4d7c01f8b
parent 27698 197f0517f0bd
child 27717 21bbd410ba04 
--- a/src/HOL/Algebra/Ideal.thy	Wed Jul 30 19:03:33 2008 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Thu Jul 31 09:49:21 2008 +0200
@@ -217,9 +217,9 @@
    apply simp
   apply (simp add: a_inv_def[symmetric])
  apply (clarsimp, rule)
-  apply (fast intro: ideal.I_l_closed ideal.intro prems)+
+  apply (fast intro: ideal.I_l_closed ideal.intro assms)+
 apply (clarsimp, rule)
- apply (fast intro: ideal.I_r_closed ideal.intro prems)+
+ apply (fast intro: ideal.I_r_closed ideal.intro assms)+
 done
 qed
isabelle