src/HOL/HOLCF/ex/Dnat.thy
changeset 45049 13efaee97111
parent 42151 4da4fc77664b
child 62175 8ffc4d0e652d
     1.1 --- a/src/HOL/HOLCF/ex/Dnat.thy	Thu Sep 22 17:15:46 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/ex/Dnat.thy	Thu Sep 22 12:55:19 2011 -0700
     1.3 @@ -61,7 +61,7 @@
     1.4     apply simp
     1.5    apply (rule allI)
     1.6    apply (case_tac y)
     1.7 -    apply (fast intro!: UU_I)
     1.8 +    apply (fast intro!: bottomI)
     1.9     apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
    1.10     apply simp
    1.11    apply (simp (no_asm_simp))