src/HOL/Integ/IntDef.thy
changeset 16770 1f1b1fae30e4
parent 16733 236dfafbeb63
child 17085 5b57f995a179
     1.1 --- a/src/HOL/Integ/IntDef.thy	Tue Jul 12 11:41:24 2005 +0200
     1.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Jul 12 11:51:31 2005 +0200
     1.3 @@ -855,17 +855,16 @@
     1.4  
     1.5  subsection {* Configuration of the code generator *}
     1.6  
     1.7 -ML {*
     1.8 -infix 7 `*;
     1.9 -infix 6 `+;
    1.10 -
    1.11 -val op `* = op * : int * int -> int;
    1.12 -val op `+ = op + : int * int -> int;
    1.13 -val `~ = ~ : int -> int;
    1.14 -*}
    1.15 +(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
    1.16  
    1.17  types_code
    1.18    "int" ("int")
    1.19 +attach (term_of) {*
    1.20 +val term_of_int = HOLogic.mk_int o IntInf.fromInt;
    1.21 +*}
    1.22 +attach (test) {*
    1.23 +fun gen_int i = one_of [~1, 1] * random_range 0 i;
    1.24 +*}
    1.25  
    1.26  constdefs
    1.27    int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
    1.28 @@ -889,9 +888,9 @@
    1.29  consts_code
    1.30    "0" :: "int"                  ("0")
    1.31    "1" :: "int"                  ("1")
    1.32 -  "uminus" :: "int => int"      ("`~")
    1.33 -  "op +" :: "int => int => int" ("(_ `+/ _)")
    1.34 -  "op *" :: "int => int => int" ("(_ `*/ _)")
    1.35 +  "uminus" :: "int => int"      ("~")
    1.36 +  "op +" :: "int => int => int" ("(_ +/ _)")
    1.37 +  "op *" :: "int => int => int" ("(_ */ _)")
    1.38    "op <" :: "int => int => bool" ("(_ </ _)")
    1.39    "op <=" :: "int => int => bool" ("(_ <=/ _)")
    1.40    "neg"                         ("(_ < 0)")