Session HOL-Nominal

Theories

• HOL-Library.Infinite_Set
• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• Nominal
  • File ‹nominal_thmdecls.ML›
  • File ‹nominal_atoms.ML›
  • File ‹nominal_permeq.ML›
  • File ‹nominal_fresh_fun.ML›
  • File ‹nominal_datatype.ML›
  • File ‹nominal_primrec.ML›
  • File ‹nominal_inductive.ML›
  • File ‹nominal_inductive2.ML›
  • File ‹nominal_induct.ML›