Theory Debt_Axiom.Debt_Axiom

theory Debt_Axiom
  imports Pure
  keywords "debt_axiomatization"  :: thy_stmt
    and    "discharge_debt_axiom" :: thy_decl
    and    "print_debt_axiom"     :: diag
    and "unspecified_type" :: thy_decl
    and "specify_type"     :: thy_decl
    and "morphisms"        :: quasi_command
begin

ML_file ‹kernel-sig.ML›
ML_file ‹kernel.ML› ― ‹the only kernel, consisting of 30 lines of ML excluding blanks›
ML_file ‹Debt_Axiom.ML›

end