equal
deleted
inserted
replaced
1 theory SigmaEx |
1 theory SigmaEx |
2 imports Nominal "../QuotMain" "../QuotList" "../QuotProd" |
2 imports Nominal "../Quotient" "../Quotient_List" "../Quotient_Product" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 datatype robj = |
7 datatype robj = |