equal
deleted
inserted
replaced
33 (Attrib.binding * term) list -> theory -> (term list * thm list) * theory |
33 (Attrib.binding * term) list -> theory -> (term list * thm list) * theory |
34 val add_primrec_overloaded: (string * (string * typ) * bool) list -> |
34 val add_primrec_overloaded: (string * (string * typ) * bool) list -> |
35 (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory -> |
35 (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory -> |
36 (term list * thm list) * theory |
36 (term list * thm list) * theory |
37 val add_primrec_simple: ((binding * typ) * mixfix) list -> term list -> |
37 val add_primrec_simple: ((binding * typ) * mixfix) list -> term list -> |
38 local_theory -> (string list * (term list * (int list * thm list))) * local_theory |
38 local_theory -> (string list * (term list * thm list)) * local_theory |
39 end; |
39 end; |
40 |
40 |
41 structure BNF_LFP_Compat : BNF_LFP_COMPAT = |
41 structure BNF_LFP_Compat : BNF_LFP_COMPAT = |
42 struct |
42 struct |
43 |
43 |
514 end; |
514 end; |
515 |
515 |
516 val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec; |
516 val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec; |
517 val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global; |
517 val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global; |
518 val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded; |
518 val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded; |
519 val add_primrec_simple = apfst (apsnd (apsnd (apsnd flat o apfst flat))) ooo |
519 val add_primrec_simple = apfst (apsnd (apsnd (flat o snd))) ooo |
520 BNF_LFP_Rec_Sugar.add_primrec_simple; |
520 BNF_LFP_Rec_Sugar.add_primrec_simple; |
521 |
521 |
522 val _ = |
522 val _ = |
523 Outer_Syntax.local_theory @{command_spec "datatype_compat"} |
523 Outer_Syntax.local_theory @{command_spec "datatype_compat"} |
524 "register new-style datatypes as old-style datatypes" |
524 "register new-style datatypes as old-style datatypes" |