|
3210
|
1 |
(* Title: HOL/Modelcheck/MCSyn.thy
|
|
|
2 |
ID: $Id$
|
|
3692
|
3 |
Author: Olaf Mueller, Jan Philipps, Robert Sandner
|
|
3210
|
4 |
Copyright 1997 TU Muenchen
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
MCSyn = MuCalculus +
|
|
|
8 |
|
|
|
9 |
syntax (Eindhoven output)
|
|
|
10 |
|
|
|
11 |
True :: bool ("TRUE")
|
|
|
12 |
False :: bool ("FALSE")
|
|
|
13 |
|
|
|
14 |
Not :: bool => bool ("NOT _" [40] 40)
|
|
|
15 |
"op &" :: [bool, bool] => bool (infixr "AND" 35)
|
|
|
16 |
"op |" :: [bool, bool] => bool (infixr "OR" 30)
|
|
|
17 |
|
|
|
18 |
"! " :: [idts, bool] => bool ("'((3A _./ _)')" [0, 10] 10)
|
|
|
19 |
"? " :: [idts, bool] => bool ("'((3E _./ _)')" [0, 10] 10)
|
|
|
20 |
"ALL " :: [idts, bool] => bool ("'((3A _./ _)')" [0, 10] 10)
|
|
|
21 |
"EX " :: [idts, bool] => bool ("'((3E _./ _)')" [0, 10] 10)
|
|
3692
|
22 |
"_lambda" :: [pttrns, 'a] => 'b ("(3L _./ _)" 10)
|
|
3210
|
23 |
|
|
3692
|
24 |
"_idts" :: [idt, idts] => idts ("_,/_" [1, 0] 0)
|
|
|
25 |
"_pattern" :: [pttrn, patterns] => pttrn ("_,/_" [1, 0] 0)
|
|
3210
|
26 |
|
|
|
27 |
"Mu " :: [idts, 'a pred] => 'a pred ("(3[mu _./ _])" 1000)
|
|
|
28 |
"Nu " :: [idts, 'a pred] => 'a pred ("(3[nu _./ _])" 1000)
|
|
|
29 |
|
|
|
30 |
oracle
|
|
|
31 |
mk_mc_oracle
|
|
|
32 |
|
|
|
33 |
end
|