src/HOL/ex/Codegenerator.thy
changeset 20713 823967ef47f1
parent 20702 8b79d853eabb
child 20807 bd3b60f9a343
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Tue Sep 26 13:34:15 2006 +0200
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Tue Sep 26 13:34:16 2006 +0200
     1.3 @@ -17,8 +17,6 @@
     1.4  subsection {* natural numbers *}
     1.5  
     1.6  definition
     1.7 -  one :: nat
     1.8 -  "one = 1"
     1.9    n :: nat
    1.10    "n = 42"
    1.11  
    1.12 @@ -105,8 +103,10 @@
    1.13  definition
    1.14    "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
    1.15  
    1.16 -code_gen xor
    1.17 -code_gen one
    1.18 +code_gen
    1.19 +  xor
    1.20 +code_gen
    1.21 +  "0::nat" "1::nat"
    1.22  code_gen
    1.23    Pair fst snd Let split swap
    1.24  code_gen "0::int" "1::int"