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/Wellfounded.thy
changeset 36635 080b755377c0
parent 35828 46cfc4b8112e
child 36664 6302f9ad7047 
--- a/src/HOL/Wellfounded.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Wellfounded.thy	Tue May 04 08:55:43 2010 +0200
@@ -68,7 +68,7 @@
   assumes lin: "OFCLASS('a::ord, linorder_class)"
   shows "OFCLASS('a::ord, wellorder_class)"
 using lin by (rule wellorder_class.intro)
-  (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
+  (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
 
 lemma (in wellorder) wf:
   "wf {(x, y). x < y}"
isabelle