--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Case_Converter.thy Sun Dec 30 10:30:41 2018 +0100
@@ -0,0 +1,23 @@
+(* Author: Pascal Stoop, ETH Zurich
+ Author: Andreas Lochbihler, Digital Asset *)
+
+theory Case_Converter
+ imports Main
+begin
+
+subsection \<open>Eliminating pattern matches\<close>
+
+definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ [code del]: "missing_pattern_match m f = f ()"
+
+lemma missing_pattern_match_cong [cong]:
+ "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
+ by(rule arg_cong)
+
+lemma missing_pattern_match_code [code_unfold]:
+ "missing_pattern_match = Code.abort"
+ unfolding missing_pattern_match_def Code.abort_def ..
+
+ML_file "case_converter.ML"
+
+end
--- a/src/HOL/Library/Code_Lazy.thy Sat Dec 29 20:32:09 2018 +0100
+++ b/src/HOL/Library/Code_Lazy.thy Sun Dec 30 10:30:41 2018 +0100
@@ -4,7 +4,7 @@
section \<open>Lazy types in generated code\<close>
theory Code_Lazy
-imports Main
+imports Case_Converter
keywords
"code_lazy_type"
"activate_lazy_type"
@@ -24,22 +24,6 @@
and thus eligible for lazification.
\<close>
-subsection \<open>Eliminating pattern matches\<close>
-
-definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
- [code del]: "missing_pattern_match m f = f ()"
-
-lemma missing_pattern_match_cong [cong]:
- "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
- by(rule arg_cong)
-
-lemma missing_pattern_match_code [code_unfold]:
- "missing_pattern_match = Code.abort"
- unfolding missing_pattern_match_def Code.abort_def ..
-
-ML_file "case_converter.ML"
-
-
subsection \<open>The type \<open>lazy\<close>\<close>
typedef 'a lazy = "UNIV :: 'a set" ..