--- 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" *}
--- a/src/HOL/Option.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Option.thy Wed Feb 12 08:35:56 2014 +0100
@@ -8,10 +8,22 @@
imports BNF_LFP Datatype Finite_Set
begin
-datatype_new 'a option = =: None | Some (the: 'a)
+datatype_new 'a option =
+ =: None
+ | Some (the: 'a)
datatype_new_compat option
+lemma [case_names None Some, cases type: option]:
+ -- {* for backward compatibility -- names of variables differ *}
+ "(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>option. y = Some option \<Longrightarrow> P) \<Longrightarrow> P"
+by (rule option.exhaust)
+
+lemma [case_names None Some, induct type: option]:
+ -- {* for backward compatibility -- names of variables differ *}
+ "P None \<Longrightarrow> (\<And>option. P (Some option)) \<Longrightarrow> P option"
+by (rule option.induct)
+
-- {* Compatibility *}
setup {* Sign.mandatory_path "option" *}