equal
deleted
inserted
replaced
1 theory NewParser |
1 theory NewParser |
2 imports "../Nominal-General/Nominal2_Base" |
2 imports "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal-General/Nominal2_Supp" |
4 "../Nominal-General/Nominal2_Supp" |
5 "Perm" "Tacs" "Equivp" "Lift" |
5 "Perm" "Tacs" "Lift" "Equivp" |
6 begin |
6 begin |
7 |
7 |
8 (* TODO |
8 (* TODO |
9 |
9 |
10 we need to also export a cases-rule for nominal datatypes |
10 we need to also export a cases-rule for nominal datatypes |