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