author | oheimb |
Fri, 25 Apr 1997 11:11:52 +0200 | |
changeset 3050 | 7eacab79b8e1 |
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