| changeset 66453 | cc19f7ca2ed6 |
| parent 59720 | f893472fff31 |
| child 67406 | 23307fd33906 |
--- a/src/Doc/Logics_ZF/If.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/Doc/Logics_ZF/If.thy Fri Aug 18 20:47:47 2017 +0200 @@ -5,7 +5,7 @@ First-Order Logic: the 'if' example. *) -theory If imports "~~/src/FOL/FOL" begin +theory If imports FOL begin definition "if" :: "[o,o,o]=>o" where "if(P,Q,R) == P&Q | ~P&R"