header {* Intuitionistic first-order logic *}

theory ONE_AXIOM = FOL :

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

local

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

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