src/HOL/Wellfounded.thy
changeset 61424 c3658c18b7bc
parent 61337 4645502c3c64
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4    assumes lin: "OFCLASS('a::ord, linorder_class)"
     1.5    shows "OFCLASS('a::ord, wellorder_class)"
     1.6  using lin by (rule wellorder_class.intro)
     1.7 -  (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
     1.8 +  (rule class.wellorder_axioms.intro, rule wf_induct_rule [OF wf], simp)
     1.9  
    1.10  lemma (in wellorder) wf:
    1.11    "wf {(x, y). x < y}"