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