equal
deleted
inserted
replaced
9 |
9 |
10 theory Ctr_Sugar |
10 theory Ctr_Sugar |
11 imports HOL |
11 imports HOL |
12 keywords |
12 keywords |
13 "print_case_translations" :: diag and |
13 "print_case_translations" :: diag and |
14 "wrap_free_constructors" :: thy_goal and |
14 "wrap_free_constructors" :: thy_goal |
15 "no_discs_sels" and |
|
16 "rep_compat" |
|
17 begin |
15 begin |
18 |
16 |
19 consts |
17 consts |
20 case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" |
18 case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" |
21 case_nil :: "'a \<Rightarrow> 'b" |
19 case_nil :: "'a \<Rightarrow> 'b" |