# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 186076d100d305c062ef97687fc4165193f5373e
# Parent  0a155051bd9dcd0f398d798a80fac9bb082a3932
compatibility names

diff -r 0a155051bd9d -r 186076d100d3 src/HOL/List.thy
--- 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" *}
 
diff -r 0a155051bd9d -r 186076d100d3 src/HOL/Option.thy
--- 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" *}