Session Incompleteness

Theories

• FinFun.FinFun
• Nominal2.Nominal2_Base
  • File ‹nominal_basics.ML›
  • File ‹nominal_thmdecls.ML›
  • File ‹nominal_permeq.ML›
  • File ‹nominal_library.ML›
  • File ‹nominal_atoms.ML›
  • File ‹nominal_eqvt.ML›
• Nominal2.Nominal2_Abs
• Nominal2.Nominal2_FCB
• Nominal2.Nominal2
  • File ‹nominal_dt_data.ML›
  • File ‹nominal_dt_rawfuns.ML›
  • File ‹nominal_dt_alpha.ML›
  • File ‹nominal_dt_quot.ML›
  • File ‹nominal_induct.ML›
  • File ‹nominal_inductive.ML›
  • File ‹nominal_function_common.ML›
  • File ‹nominal_function_core.ML›
  • File ‹nominal_mutual.ML›
  • File ‹nominal_function.ML›
  • File ‹nominal_termination.ML›
• SyntaxN
• Coding
• Predicates
• Sigma
• Coding_Predicates
• Pf_Predicates
• Functions
• Goedel_I
• II_Prelims
• Pseudo_Coding
• Quote
• Goedel_II