author | wenzelm |
Sat, 16 Jul 2016 00:11:03 +0200 | |
changeset 63512 | 1c7b1e294fb5 |
parent 63511 | 1c2c045decb3 |
child 63513 | 9f8d06f23c09 |
--- a/src/Pure/Isar/rule_cases.ML Fri Jul 15 23:47:07 2016 +0200 +++ b/src/Pure/Isar/rule_cases.ML Sat Jul 16 00:11:03 2016 +0200 @@ -12,7 +12,9 @@ binds: (indexname * term option) list, cases: (string * T) list} type cases = (string * T option) list + val case_conclN: string val case_hypsN: string + val case_premsN: string val strip_params: term -> (string * typ) list type info = ((string * string list) * string list) list val make_common: Proof.context -> term -> info -> cases