src/HOLCF/Discrete.thy
changeset 25131 2c8caac48ade
parent 19105 3aabd46340e0
child 25782 2d8b845dc298
     1.1 --- a/src/HOLCF/Discrete.thy	Sun Oct 21 14:21:45 2007 +0200
     1.2 +++ b/src/HOLCF/Discrete.thy	Sun Oct 21 14:21:48 2007 +0200
     1.3 @@ -56,9 +56,9 @@
     1.4  
     1.5  subsection {* @{term undiscr} *}
     1.6  
     1.7 -constdefs
     1.8 -   undiscr :: "('a::type)discr => 'a"
     1.9 -  "undiscr x == (case x of Discr y => y)"
    1.10 +definition
    1.11 +  undiscr :: "('a::type)discr => 'a" where
    1.12 +  "undiscr x = (case x of Discr y => y)"
    1.13  
    1.14  lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
    1.15  by (simp add: undiscr_def)