| changeset 1851 | d25e1576ca82 |
| parent 1848 | acacc448f9ea |
| child 1852 | 13bc3f41ad8d |
| 1850:05b2dd2b0e8a | 1851:d25e1576ca82 |
|---|---|
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 ***} |