equal
deleted
inserted
replaced
|
1 structure If = |
|
2 struct |
|
3 |
|
4 local |
|
5 val parse_ast_translation = [] |
|
6 val parse_preproc = None |
|
7 val parse_postproc = None |
|
8 val parse_translation = [] |
|
9 val print_translation = [] |
|
10 val print_preproc = None |
|
11 val print_postproc = None |
|
12 val print_ast_translation = [] |
|
13 in |
|
14 |
|
15 (**** begin of user section ****) |
|
16 |
|
17 (**** end of user section ****) |
|
18 |
|
19 val thy = extend_theory (FOL.thy) |
|
20 "If" |
|
21 ([], |
|
22 [], |
|
23 [], |
|
24 [], |
|
25 [(["if"], "[o,o,o]=>o")], |
|
26 None) |
|
27 [("if_def", "if(P,Q,R) == P&Q | ~P&R")] |
|
28 |
|
29 val ax = get_axiom thy |
|
30 |
|
31 val if_def = ax "if_def" |
|
32 |
|
33 |
|
34 end |
|
35 end |