author | wenzelm |
Mon, 20 Oct 1997 12:50:18 +0200 | |
changeset 3954 | c8c188655948 |
parent 0 | a5a9c433f639 |
permissions | -rw-r--r-- |
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