src/HOL/Inductive.thy
 changeset 54398 100c0eaf63d5 parent 52143 36ffe23b25f8 child 54615 62fb5af93fe2
```     1.1 --- a/src/HOL/Inductive.thy	Tue Nov 12 13:47:24 2013 +0100
1.2 +++ b/src/HOL/Inductive.thy	Tue Nov 12 13:47:24 2013 +0100
1.3 @@ -4,12 +4,12 @@
1.4
1.5  header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}
1.6
1.7 -theory Inductive
1.8 -imports Complete_Lattices
1.9 +theory Inductive
1.10 +imports Complete_Lattices Ctr_Sugar
1.11  keywords
1.12    "inductive" "coinductive" :: thy_decl and
1.13    "inductive_cases" "inductive_simps" :: thy_script and "monos" and
1.14 -  "print_inductives" "print_case_translations" :: diag and
1.15 +  "print_inductives" :: diag and
1.16    "rep_datatype" :: thy_goal and
1.17    "primrec" :: thy_decl
1.18  begin
1.19 @@ -30,7 +30,7 @@
1.20
1.21  subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *}
1.22
1.23 -text{*@{term "lfp f"} is the least upper bound of
1.24 +text{*@{term "lfp f"} is the least upper bound of
1.25        the set @{term "{u. f(u) \<le> u}"} *}
1.26
1.27  lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
1.28 @@ -273,21 +273,6 @@
1.29  ML_file "Tools/Datatype/datatype_aux.ML"
1.30  ML_file "Tools/Datatype/datatype_prop.ML"
1.31  ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
1.32 -
1.33 -consts
1.34 -  case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
1.35 -  case_nil :: "'a \<Rightarrow> 'b"
1.36 -  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
1.37 -  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
1.38 -  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
1.39 -declare [[coercion_args case_guard - + -]]
1.40 -declare [[coercion_args case_cons - -]]
1.41 -declare [[coercion_args case_abs -]]
1.42 -declare [[coercion_args case_elem - +]]
1.43 -
1.44 -ML_file "Tools/case_translation.ML"
1.45 -setup Case_Translation.setup
1.46 -
1.47  ML_file "Tools/Datatype/rep_datatype.ML"
1.48  ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
1.49  ML_file "Tools/Datatype/primrec.ML"
```