equal
deleted
inserted
replaced
8 |
8 |
9 theory Intensional |
9 theory Intensional |
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 classes world |
13 class world |
14 classrel world < type |
|
15 |
14 |
16 (** abstract syntax **) |
15 (** abstract syntax **) |
17 |
16 |
18 type_synonym ('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *) |
17 type_synonym ('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *) |
19 type_synonym 'w form = "('w, bool) expr" |
18 type_synonym 'w form = "('w, bool) expr" |