equal
deleted
inserted
replaced
1 (* Title: ZF/IMP/Bexp.ML |
|
2 ID: $Id$ |
|
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
4 Copyright 1994 TUM |
|
5 *) |
|
6 |
|
7 structure Bexp = Datatype_Fun |
|
8 ( |
|
9 val thy = Aexp.thy; |
|
10 val thy_name = "Bexp" |
|
11 val rec_specs = |
|
12 [ |
|
13 ( |
|
14 "bexp", "univ(aexp Un ((nat*nat)->bool) )", |
|
15 [ |
|
16 ( ["true","false"], "i", NoSyn), |
|
17 ( ["noti"], "i => i", NoSyn), |
|
18 ( ["andi"], "[i,i]=>i", Infixl 60), |
|
19 ( ["ori"], "[i,i]=>i", Infixl 60), |
|
20 ( ["ROp"], "[i,i,i] => i", NoSyn) |
|
21 ] |
|
22 ) |
|
23 ]; |
|
24 |
|
25 val rec_styp = "i"; |
|
26 val sintrs = |
|
27 [ |
|
28 "true : bexp", |
|
29 "false : bexp", |
|
30 "[| a0 : aexp; a1 : aexp; f: (nat*nat)->bool |] ==> ROp(f,a0,a1) : bexp", |
|
31 "b : bexp ==> noti(b) : bexp", |
|
32 "[| b0 : bexp; b1 : bexp |] ==> b0 andi b1 : bexp", |
|
33 "[| b0 : bexp; b1 : bexp |] ==> b0 ori b1 : bexp" |
|
34 ]; |
|
35 val monos = []; |
|
36 val type_intrs = datatype_intrs; |
|
37 val type_elims = datatype_elims; |
|
38 ); |
|