equal
deleted
inserted
replaced
8 |
8 |
9 Fun = Vimage + equalities + |
9 Fun = Vimage + equalities + |
10 |
10 |
11 instance set :: (term) order |
11 instance set :: (term) order |
12 (subset_refl,subset_trans,subset_antisym,psubset_eq) |
12 (subset_refl,subset_trans,subset_antisym,psubset_eq) |
13 nonterminals |
|
14 updbinds updbind |
|
15 |
|
16 consts |
13 consts |
17 fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
14 fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
18 |
15 |
|
16 nonterminals |
|
17 updbinds updbind |
19 syntax |
18 syntax |
20 |
|
21 (* Let expressions *) |
|
22 |
|
23 "_updbind" :: ['a, 'a] => updbind ("(2_ :=/ _)") |
19 "_updbind" :: ['a, 'a] => updbind ("(2_ :=/ _)") |
24 "" :: updbind => updbinds ("_") |
20 "" :: updbind => updbinds ("_") |
25 "_updbinds" :: [updbind, updbinds] => updbinds ("_,/ _") |
21 "_updbinds" :: [updbind, updbinds] => updbinds ("_,/ _") |
26 "_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [1000,0] 900) |
22 "_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [1000,0] 900) |
27 |
23 |