equal
deleted
inserted
replaced
13 val case_names: string list -> 'a attribute |
13 val case_names: string list -> 'a attribute |
14 val save: thm -> thm -> thm |
14 val save: thm -> thm -> thm |
15 val get: thm -> string list * int |
15 val get: thm -> string list * int |
16 val add: thm -> thm * (string list * int) |
16 val add: thm -> thm * (string list * int) |
17 type T |
17 type T |
|
18 val strip_params: term -> (string * typ) list |
18 val make: bool -> term option -> theory * term -> string list -> (string * T option) list |
19 val make: bool -> term option -> theory * term -> string list -> (string * T option) list |
19 val simple: bool -> theory * term -> string -> string * T option |
20 val simple: bool -> theory * term -> string -> string * T option |
20 val rename_params: string list list -> thm -> thm |
21 val rename_params: string list list -> thm -> thm |
21 val params: string list list -> 'a attribute |
22 val params: string list list -> 'a attribute |
22 type tactic |
23 type tactic |
93 type T = |
94 type T = |
94 {fixes: (string * typ) list, |
95 {fixes: (string * typ) list, |
95 assumes: (string * term list) list, |
96 assumes: (string * term list) list, |
96 binds: (indexname * term option) list}; |
97 binds: (indexname * term option) list}; |
97 |
98 |
98 fun unskolem x = |
99 val strip_params = |
99 (case try Syntax.dest_skolem x of SOME x' => x' | NONE => x); |
100 Logic.strip_params #> map (fn (x, T) => (the_default x (try Syntax.dest_skolem x), T)); |
100 |
101 |
101 fun prep_case is_open thy (split, raw_prop) name = |
102 fun prep_case is_open thy (split, raw_prop) name = |
102 let |
103 let |
103 val prop = Drule.norm_hhf thy raw_prop; |
104 val prop = Drule.norm_hhf thy raw_prop; |
104 |
105 |
105 val xs = map (apfst unskolem) (Logic.strip_params prop); |
106 val xs = strip_params prop; |
106 val rename = if is_open then I else map (apfst Syntax.internal); |
107 val rename = if is_open then I else map (apfst Syntax.internal); |
107 val named_xs = |
108 val named_xs = |
108 (case split of |
109 (case split of |
109 NONE => rename xs |
110 NONE => rename xs |
110 | SOME t => |
111 | SOME t => |