equal
deleted
inserted
replaced
10 {fixes: (binding * typ) list, |
10 {fixes: (binding * typ) list, |
11 assumes: (string * term list) list, |
11 assumes: (string * term list) list, |
12 binds: (indexname * term option) list, |
12 binds: (indexname * term option) list, |
13 cases: (string * T) list} |
13 cases: (string * T) list} |
14 type cases = (string * T option) list |
14 type cases = (string * T option) list |
|
15 val case_conclN: string |
15 val case_hypsN: string |
16 val case_hypsN: string |
|
17 val case_premsN: string |
16 val strip_params: term -> (string * typ) list |
18 val strip_params: term -> (string * typ) list |
17 type info = ((string * string list) * string list) list |
19 type info = ((string * string list) * string list) list |
18 val make_common: Proof.context -> term -> info -> cases |
20 val make_common: Proof.context -> term -> info -> cases |
19 val make_nested: Proof.context -> term -> term -> info -> cases |
21 val make_nested: Proof.context -> term -> term -> info -> cases |
20 val apply: term list -> T -> T |
22 val apply: term list -> T -> T |