new datatype theory, supports 'draft theories' and incremental extension:
add_classes, add_defsort, add_types, add_tyabbrs, add_tyabbrs_i,
add_arities, add_consts, add_consts_i, add_syntax, add_syntax_i,
add_trfuns, add_trrules, add_axioms, add_axioms_i, add_thyname;
added merge_thy_list for multiple merges and extend-merges;
added rep_theory, subthy, eq_thy, cert_axm, read_axm;
changed type of axioms_of;
renamed internal merge_theories to merge_thm_sgs;
various internal changes of thm and theory related code;
(* Title: Pure/Thy/ROOT
ID: $Id$
Author: Sonia Mahjoub / Tobias Nipkow
Copyright 1992 TU Muenchen
This file builds the theory parser.
It assumes the standard Isabelle environment.
*)
use "scan.ML";
use "parse.ML";
use "syntax.ML";
use "read.ML";
structure Keyword =
struct
val alphas = ["classes", "default", "arities", "types",
"consts", "rules", "end", "rules", "mixfix",
"infixr", "infixl", "binder", "translations"]
val symbols = [",", "<", "{", "}", "(", ")", "(*", "*)",
"[", "]", "::", "=", "+", "==", "=>", "<="]
end;
structure Lex = LexicalFUN (Keyword);
structure Parse = ParseFUN (Lex);
structure ThySyn = ThySynFUN (Parse);
(*This structure is only defined to be compatible with older versions of
READTHY. Don't use it in newly created theory/ROOT.ML files! Instead
define a new structure. Otherwise Poly/ML won't save a reference variable
defined inside the functor. *)
structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
open Readthy;