Skip to content
Success

Changes

Summary

  1. Nominal2: permute definition and pt instance proof handle indirect recursion
Changeset 9096:d2f502a794b7 by huffman:
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)