changeset 45606 | b1e1508643b1 |
parent 42151 | 4da4fc77664b |
child 46950 | d0181abdbdac |
--- a/src/HOL/HOLCF/Cpodef.thy Sun Nov 20 21:05:23 2011 +0100 +++ b/src/HOL/HOLCF/Cpodef.thy Sun Nov 20 21:07:06 2011 +0100 @@ -107,7 +107,7 @@ by (rule typedef_is_lubI [OF below]) qed -lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard] +lemmas typedef_lub = typedef_is_lub [THEN lub_eqI] theorem typedef_cpo: fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"