| changeset 65449 | c82e63b11b8b |
| parent 46822 | 95f1e700b712 |
| child 76213 | e44d86131648 |
--- a/src/ZF/ex/Commutation.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/ex/Commutation.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ Commutation theory for proving the Church Rosser theorem. *) -theory Commutation imports Main begin +theory Commutation imports ZF begin definition square :: "[i, i, i, i] => o" where