| changeset 17480 | fd19f77dcf60 |
| parent 0 | a5a9c433f639 |
| child 19796 | d86e7b1fc472 |
| 17479:68a7acb5f22e | 17480:fd19f77dcf60 |
|---|---|
1 If = FOLP + |
1 (* $Id$ *) |
2 consts if :: "[o,o,o]=>o" |
2 |
3 rules |
3 theory If |
4 if_def "if(P,Q,R) == P&Q | ~P&R" |
4 imports FOLP |
5 begin |
|
6 |
|
7 constdefs |
|
8 if :: "[o,o,o]=>o" |
|
9 "if(P,Q,R) == P&Q | ~P&R" |
|
10 |
|
11 ML {* use_legacy_bindings (the_context ()) *} |
|
12 |
|
5 end |
13 end |