src/Pure/Isar/rule_cases.ML
changeset 63512 1c7b1e294fb5
parent 61853 fb7756087101
child 67559 833d154ab189
--- 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