codatatypes are not datatypes
authorblanchet
Wed Sep 03 00:06:18 2014 +0200 (2014-09-03)
changeset 58146d91c1e50b36e
parent 58145 3cfbb68ad2e0
child 58147 967444d352b8
codatatypes are not datatypes
src/HOL/Complex.thy
src/HOL/Tools/BNF/bnf_lfp_compat.ML
     1.1 --- a/src/HOL/Complex.thy	Wed Sep 03 00:06:17 2014 +0200
     1.2 +++ b/src/HOL/Complex.thy	Wed Sep 03 00:06:18 2014 +0200
     1.3 @@ -11,11 +11,9 @@
     1.4  begin
     1.5  
     1.6  text {*
     1.7 -
     1.8 -We use the @{text codatatype}-command to define the type of complex numbers. This might look strange
     1.9 -at first, but allows us to use @{text primcorec} to define complex-functions by defining their
    1.10 -real and imaginary result separate.
    1.11 -
    1.12 +We use the @{text codatatype} command to define the type of complex numbers. This allows us to use
    1.13 +@{text primcorec} to define complex functions by defining their real and imaginary result
    1.14 +separately.
    1.15  *}
    1.16  
    1.17  codatatype complex = Complex (Re: real) (Im: real)
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 03 00:06:17 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 03 00:06:18 2014 +0200
     2.3 @@ -265,8 +265,9 @@
     2.4  
     2.5  fun new_interpretation_of nesting_pref f (fp_sugars : fp_sugar list) thy =
     2.6    let val T_names = map (fst o dest_Type o #T) fp_sugars in
     2.7 -    if nesting_pref = Keep_Nesting orelse
     2.8 -        exists (is_none o Old_Datatype_Data.get_info thy) T_names then
     2.9 +    if forall (curry (op =) Least_FP o #fp) fp_sugars andalso
    2.10 +        (nesting_pref = Keep_Nesting orelse
    2.11 +         exists (is_none o Old_Datatype_Data.get_info thy) T_names) then
    2.12        f Old_Datatype_Aux.default_config T_names thy
    2.13      else
    2.14        thy