src/HOL/HOLCF/Completion.thy
changeset 61169 4de9ff3ea29a
parent 58880 0baae4311a9f
child 62175 8ffc4d0e652d
     1.1 --- a/src/HOL/HOLCF/Completion.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/Completion.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4    assumes type: "type_definition Rep Abs {S. ideal S}"
     1.5    assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
     1.6    shows "OFCLASS('b, cpo_class)"
     1.7 -by (default, rule exI, erule typedef_ideal_lub [OF type below])
     1.8 +  by standard (rule exI, erule typedef_ideal_lub [OF type below])
     1.9  
    1.10  end
    1.11