header {* Intuitionistic first-order logic *}

theory ONE_RULE = FOL :

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

local

subsection {* Lemmas and proof tools *}
  
axioms
  
  myrule:      ""

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