equal
deleted
inserted
replaced
1 theory FSet2 |
1 theory FSet2 |
2 imports "../QuotMain" "../QuotList" List |
2 imports "../Quotient" "../Quotient_List" List |
3 begin |
3 begin |
4 |
4 |
5 inductive |
5 inductive |
6 list_eq (infix "\<approx>" 50) |
6 list_eq (infix "\<approx>" 50) |
7 where |
7 where |