insert std/L.mli

theory K.
  include theory L.

  formal system. 
    formula A, B, C  term t  metaobject x.

  [* Axioms 1-3 of Mendelson, p.57, are here included from theory L
     where they are named L1, L2, L3. Modus ponens (MP) is likewise
     included from theory L. Mendelson axioms 4 (resp. 5)
     are here called K1 (resp. K2). *]

  -- Treated as axioms in Mendelson:
  rule K1. t free for x in A ⊢ (∀x A) ⇒ A[x.t].
  rule K1a. ∀x A ⊢ A[x.t].
  rule K2. x not free in A ⊢ (∀x: A ⇒ B) ⇒ (A ⇒ ∀x B).
  
  rule Gen. A ⊢ ∀x A. -- Generalization.

  end formal system.

end theory K.