equal
deleted
inserted
replaced
37 val delsplits : simpset * thm list -> simpset |
37 val delsplits : simpset * thm list -> simpset |
38 val Addsplits : thm list -> unit |
38 val Addsplits : thm list -> unit |
39 val Delsplits : thm list -> unit |
39 val Delsplits : thm list -> unit |
40 val split_add: attribute |
40 val split_add: attribute |
41 val split_del: attribute |
41 val split_del: attribute |
42 val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list |
42 val split_modifiers : Method.modifier parser list |
43 val setup: theory -> theory |
43 val setup: theory -> theory |
44 end; |
44 end; |
45 |
45 |
46 functor SplitterFun(Data: SPLITTER_DATA): SPLITTER = |
46 functor SplitterFun(Data: SPLITTER_DATA): SPLITTER = |
47 struct |
47 struct |