equal
deleted
inserted
replaced
11 *) |
11 *) |
12 |
12 |
13 Intensional = Main + |
13 Intensional = Main + |
14 |
14 |
15 axclass |
15 axclass |
16 world < term |
16 world < type |
17 |
17 |
18 (** abstract syntax **) |
18 (** abstract syntax **) |
19 |
19 |
20 types |
20 types |
21 ('w,'a) expr = 'w => 'a (* intention: 'w::world, 'a::term *) |
21 ('w,'a) expr = 'w => 'a (* intention: 'w::world, 'a::type *) |
22 'w form = ('w, bool) expr |
22 'w form = ('w, bool) expr |
23 |
23 |
24 consts |
24 consts |
25 Valid :: ('w::world) form => bool |
25 Valid :: ('w::world) form => bool |
26 const :: 'a => ('w::world, 'a) expr |
26 const :: 'a => ('w::world, 'a) expr |