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.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
```