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"