equal
deleted
inserted
replaced
17 number < "term" (*for numeric types: nat, int, real, ...*) |
17 number < "term" (*for numeric types: nat, int, real, ...*) |
18 |
18 |
19 consts |
19 consts |
20 number_of :: "bin => 'a::number" |
20 number_of :: "bin => 'a::number" |
21 |
21 |
22 nonterminals |
|
23 numeral |
|
24 |
|
25 syntax |
22 syntax |
26 "_constify" :: "num => numeral" ("_") |
23 "_Numeral" :: "num_const => 'a" ("_") |
27 "_Numeral" :: "numeral => 'a" ("_") |
|
28 Numeral0 :: 'a |
24 Numeral0 :: 'a |
29 Numeral1 :: 'a |
25 Numeral1 :: 'a |
30 |
26 |
31 translations |
27 translations |
32 "Numeral0" == "number_of Pls" |
28 "Numeral0" == "number_of Pls" |