src/HOL/Code_Numeral.thy
changeset 60758 d8d85a8172b5
parent 60562 24af00b010cf
child 60868 dd18c33c001e
     1.1 --- a/src/HOL/Code_Numeral.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -2,13 +2,13 @@
     1.4      Author:     Florian Haftmann, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Numeric types for code generation onto target language numerals only *}
     1.8 +section \<open>Numeric types for code generation onto target language numerals only\<close>
     1.9  
    1.10  theory Code_Numeral
    1.11  imports Nat_Transfer Divides Lifting
    1.12  begin
    1.13  
    1.14 -subsection {* Type of target language integers *}
    1.15 +subsection \<open>Type of target language integers\<close>
    1.16  
    1.17  typedef integer = "UNIV \<Colon> int set"
    1.18    morphisms int_of_integer integer_of_int ..
    1.19 @@ -238,9 +238,9 @@
    1.20    "integer_of_nat (numeral n) = numeral n"
    1.21  by transfer simp
    1.22  
    1.23 -subsection {* Code theorems for target language integers *}
    1.24 +subsection \<open>Code theorems for target language integers\<close>
    1.25  
    1.26 -text {* Constructors *}
    1.27 +text \<open>Constructors\<close>
    1.28  
    1.29  definition Pos :: "num \<Rightarrow> integer"
    1.30  where
    1.31 @@ -261,7 +261,7 @@
    1.32  code_datatype "0::integer" Pos Neg
    1.33  
    1.34  
    1.35 -text {* Auxiliary operations *}
    1.36 +text \<open>Auxiliary operations\<close>
    1.37  
    1.38  lift_definition dup :: "integer \<Rightarrow> integer"
    1.39    is "\<lambda>k::int. k + k"
    1.40 @@ -290,7 +290,7 @@
    1.41    by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+
    1.42  
    1.43  
    1.44 -text {* Implementations *}
    1.45 +text \<open>Implementations\<close>
    1.46  
    1.47  lemma one_integer_code [code, code_unfold]:
    1.48    "1 = Pos Num.One"
    1.49 @@ -520,7 +520,7 @@
    1.50  hide_const (open) Pos Neg sub dup divmod_abs
    1.51  
    1.52  
    1.53 -subsection {* Serializer setup for target language integers *}
    1.54 +subsection \<open>Serializer setup for target language integers\<close>
    1.55  
    1.56  code_reserved Eval int Integer abs
    1.57  
    1.58 @@ -541,12 +541,12 @@
    1.59      and (Haskell) "!(0/ ::/ Integer)"
    1.60      and (Scala) "BigInt(0)"
    1.61  
    1.62 -setup {*
    1.63 +setup \<open>
    1.64    fold (fn target =>
    1.65      Numeral.add_code @{const_name Code_Numeral.Pos} I Code_Printer.literal_numeral target
    1.66      #> Numeral.add_code @{const_name Code_Numeral.Neg} (op ~) Code_Printer.literal_numeral target)
    1.67      ["SML", "OCaml", "Haskell", "Scala"]
    1.68 -*}
    1.69 +\<close>
    1.70  
    1.71  code_printing
    1.72    constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
    1.73 @@ -613,7 +613,7 @@
    1.74    code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
    1.75  
    1.76  
    1.77 -subsection {* Type of target language naturals *}
    1.78 +subsection \<open>Type of target language naturals\<close>
    1.79  
    1.80  typedef natural = "UNIV \<Colon> nat set"
    1.81    morphisms nat_of_natural natural_of_nat ..
    1.82 @@ -787,7 +787,7 @@
    1.83    by (rule is_measure_trivial)
    1.84  
    1.85  
    1.86 -subsection {* Inductive representation of target language naturals *}
    1.87 +subsection \<open>Inductive representation of target language naturals\<close>
    1.88  
    1.89  lift_definition Suc :: "natural \<Rightarrow> natural"
    1.90    is Nat.Suc
    1.91 @@ -831,7 +831,7 @@
    1.92  hide_const (open) Suc
    1.93  
    1.94  
    1.95 -subsection {* Code refinement for target language naturals *}
    1.96 +subsection \<open>Code refinement for target language naturals\<close>
    1.97  
    1.98  lift_definition Nat :: "integer \<Rightarrow> natural"
    1.99    is nat