Session Rhombus_HOL_Kernel

Theories

• Rhombus_HOL_Syntax
• Rhombus_HOL_Substitution
• Rhombus_HOL_Kernel
• Rhombus_HOL_Semantics
• Rhombus_HOL_Soundness
• Rhombus_HOL_Extension_Core
• Rhombus_HOL_Extensions
• Rhombus_HOL_Base_Model
• Rhombus_HOL_Adequacy
• Rhombus_HOL_Countermodels
• Rhombus_HOL_Audit
• Rhombus_HOL_Nat_Extension
• Rhombus_HOL_Code_API
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Int
• HOL-Library.Code_Target_Numeral
• Rhombus_HOL_Code_Export
  • File ‹Rhombus_HOL_Code_Target.ML›