changeset 40815 | 6e2d17cc0d1d |
parent 39302 | d7728f65b353 |
child 45542 | 4849dbe6e310 |
--- a/src/HOL/NSA/StarDef.thy Mon Nov 29 12:15:14 2010 +0100 +++ b/src/HOL/NSA/StarDef.thy Mon Nov 29 13:44:54 2010 +0100 @@ -62,7 +62,7 @@ by (simp add: starrel_def) lemma equiv_starrel: "equiv UNIV starrel" -proof (rule equiv.intro) +proof (rule equivI) show "refl starrel" by (simp add: refl_on_def) show "sym starrel" by (simp add: sym_def eq_commute) show "trans starrel" by (auto intro: transI elim!: ultra)