equal
deleted
inserted
replaced
9 (*Example of a datatype with an infix constructor*) |
9 (*Example of a datatype with an infix constructor*) |
10 structure Bin = Datatype_Fun |
10 structure Bin = Datatype_Fun |
11 (val thy = Univ.thy; |
11 (val thy = Univ.thy; |
12 val rec_specs = |
12 val rec_specs = |
13 [("bin", "univ(0)", |
13 [("bin", "univ(0)", |
14 [(["Plus", "Minus"], "i"), |
14 [(["Plus", "Minus"], "i", NoSyn), |
15 (["op $$"], "[i,i]=>i")])]; |
15 (["$$"], "[i,i]=>i", Infixl 60)])]; |
16 val rec_styp = "i"; |
16 val rec_styp = "i"; |
17 val ext = Some (Syntax.simple_sext |
|
18 [OldMixfix.Infixl("$$", "[i,i] => i", 60)]); |
|
19 val sintrs = |
17 val sintrs = |
20 ["Plus : bin", |
18 ["Plus : bin", |
21 "Minus : bin", |
19 "Minus : bin", |
22 "[| w: bin; b: bool |] ==> w$$b : bin"]; |
20 "[| w: bin; b: bool |] ==> w$$b : bin"]; |
23 val monos = []; |
21 val monos = []; |