header {* Intuitionistic first-order logic *}

theory ONE_AXIOM = FOL :

subsection  {* Syntax and axiomatic basis *}
  
consts
  
  R           :: "'a => o"
  S           :: "'a => o"
  T           :: "'a => o"

local

subsection {* Lemmas and proof tools *}
  
axioms
  
  myaxiom:      "ALL x. R(x) & S(x) --> T(x)"

ML
{*
  val myaxiom = thm "myaxiom";
*}  
end