src/FOL/.fol.thy.ML
author paulson
Thu, 21 Mar 1996 13:02:26 +0100
changeset 1601 0ef6ea27ab15
parent 0 a5a9c433f639
permissions -rw-r--r--
Changes required by removal of the theory argument of Theorem

structure FOL =
struct

local
 val parse_ast_translation = []
 val parse_preproc = None
 val parse_postproc = None
 val parse_translation = []
 val print_translation = []
 val print_preproc = None
 val print_postproc = None
 val print_ast_translation = []
in

(**** begin of user section ****)

(**** end of user section ****)

val thy = extend_theory (IFOL.thy)
 "FOL"
 ([],
  [],
  [],
  [],
  [],
  None)
 [("classical", "(~P ==> P) ==> P")]

val ax = get_axiom thy

val classical = ax "classical"


end
end