1826
|
1 |
local open Ast;
|
|
2 |
fun bigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] =
|
|
3 |
fold_ast_p "êë" (unfold_ast "_asms" asms, concl)
|
|
4 |
| bigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
|
|
5 |
fun impl_ast_tr' (*"êë"*) asts =
|
|
6 |
(case unfold_ast_p "êë" (Appl (Constant "êë" :: asts)) of
|
|
7 |
(asms as _ :: _ :: _, concl)
|
|
8 |
=> Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl]
|
|
9 |
| _ => raise Match);
|
|
10 |
|
|
11 |
in
|
|
12 |
val parse_ast_translation = ("Gbigimpl", bigimpl_ast_tr)::
|
|
13 |
("Glam", fn asts => Appl (Constant "_abs" :: asts))::
|
|
14 |
parse_ast_translation;
|
|
15 |
|
|
16 |
val print_ast_translation = ("êë", impl_ast_tr')::
|
|
17 |
("_lambda", fn asts => Appl (Constant "Glam" :: asts)) ::
|
|
18 |
print_ast_translation;
|
|
19 |
|
|
20 |
end;
|
|
21 |
|
|
22 |
local open Syntax in
|
|
23 |
val thy = thy
|
|
24 |
|> add_trrules_i
|
|
25 |
[mk_appl (Constant "Ú" ) [Variable "P", Variable "Q"] <->
|
|
26 |
mk_appl (Constant "==") [Variable "P", Variable "Q"],
|
|
27 |
mk_appl (Constant "êë" ) [Variable "P", Variable "Q"] <->
|
|
28 |
mk_appl (Constant "==>") [Variable "P", Variable "Q"],
|
|
29 |
(Constant "Ä" ) <-> (Constant "!!")]
|
|
30 |
end;
|