Summary
- Nominal2: permute definition and pt instance proof handle indirect recursion
The file was modified | thys/Nominal2/Nominal2.thy (diff) |
The file was modified | thys/Nominal2/nominal_dt_data.ML (diff) |
The file was modified | thys/Nominal2/nominal_dt_rawfuns.ML (diff) |