tuned signature;
authorwenzelm
Sat, 16 Jul 2016 00:11:03 +0200
changeset 63512 1c7b1e294fb5
parent 63511 1c2c045decb3
child 63513 9f8d06f23c09
tuned signature;
src/Pure/Isar/rule_cases.ML
--- 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