| changeset 55380 | 4de48353034e |
| parent 53367 | 1f383542226b |
| child 56036 | 6c3fc3b5592a |
| 55379:9701dbc35f86 | 55380:4de48353034e |
|---|---|
6 |
6 |
7 theory Locale_Test1 |
7 theory Locale_Test1 |
8 imports FOL |
8 imports FOL |
9 begin |
9 begin |
10 |
10 |
11 typedecl int arities int :: "term" |
11 typedecl int |
12 instance int :: "term" .. |
|
13 |
|
12 consts plus :: "int => int => int" (infixl "+" 60) |
14 consts plus :: "int => int => int" (infixl "+" 60) |
13 zero :: int ("0") |
15 zero :: int ("0") |
14 minus :: "int => int" ("- _") |
16 minus :: "int => int" ("- _") |
15 |
17 |
16 axiomatization where |
18 axiomatization where |