| changeset 1848 | acacc448f9ea |
| parent 1592 | b679900fa5f6 |
| child 1852 | 13bc3f41ad8d |
| 1846:756982b4fe20 | 1848:acacc448f9ea |
|---|---|
1 theory Term4 |
1 theory Term4 |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" "Quotient_List" |
2 imports "../Abs" "../Perm" "../Fv" "../Rsp" "Quotient_List" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 section {*** lam with indirect list recursion ***} |
7 section {*** lam with indirect list recursion ***} |