equal
deleted
inserted
replaced
1 theory QuotScript |
1 theory QuotScript |
2 imports Plain ATP_Linkup |
2 imports Plain ATP_Linkup Predicate |
3 begin |
3 begin |
4 |
4 |
5 definition |
5 definition |
6 "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)" |
6 "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)" |
7 |
7 |