src/HOL/Ctr_Sugar.thy
changeset 57631 959caab43a3d
parent 55971 7644d63e8c3f
child 58177 166131276380
     1.1 --- a/src/HOL/Ctr_Sugar.thy	Thu Jul 24 00:24:00 2014 +0200
     1.2 +++ b/src/HOL/Ctr_Sugar.thy	Thu Jul 24 00:24:00 2014 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
     1.5    case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
     1.6    case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
     1.7 +
     1.8  declare [[coercion_args case_guard - + -]]
     1.9  declare [[coercion_args case_cons - -]]
    1.10  declare [[coercion_args case_abs -]]