equal
deleted
inserted
replaced
15 |
15 |
16 header{*Arithmetic on Binary Integers*} |
16 header{*Arithmetic on Binary Integers*} |
17 |
17 |
18 theory Bin |
18 theory Bin |
19 imports Int_ZF Datatype_ZF |
19 imports Int_ZF Datatype_ZF |
20 uses ("Tools/numeral_syntax.ML") |
|
21 begin |
20 begin |
22 |
21 |
23 consts bin :: i |
22 consts bin :: i |
24 datatype |
23 datatype |
25 "bin" = Pls |
24 "bin" = Pls |
102 NCons(bin_mult(v,w),0))" |
101 NCons(bin_mult(v,w),0))" |
103 |
102 |
104 syntax |
103 syntax |
105 "_Int" :: "xnum_token => i" ("_") |
104 "_Int" :: "xnum_token => i" ("_") |
106 |
105 |
107 use "Tools/numeral_syntax.ML" |
106 ML_file "Tools/numeral_syntax.ML" |
108 setup Numeral_Syntax.setup |
107 setup Numeral_Syntax.setup |
109 |
108 |
110 |
109 |
111 declare bin.intros [simp,TC] |
110 declare bin.intros [simp,TC] |
112 |
111 |