src/HOL/List.thy
changeset 55406 186076d100d3
parent 55405 0a155051bd9d
child 55415 05f5fdb8d093
--- a/src/HOL/List.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/List.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -14,6 +14,18 @@
 
 datatype_new_compat list
 
+thm list.exhaust[no_vars]
+
+lemma [case_names Nil Cons, cases type: list]:
+  -- {* for backward compatibility -- names of variables differ *}
+  "(y = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>a list. y = a # list \<Longrightarrow> P) \<Longrightarrow> P"
+by (rule list.exhaust)
+
+lemma [case_names Nil Cons, induct type: list]:
+  -- {* for backward compatibility -- names of variables differ *}
+  "P [] \<Longrightarrow> (\<And>a list. P list \<Longrightarrow> P (a # list)) \<Longrightarrow> P list"
+by (rule list.induct)
+
 -- {* Compatibility *}
 setup {* Sign.mandatory_path "list" *}