simpset is hidden in a functor now.

Internale optimization of the simplifier: in case a subterm stays unchanged, None is returned. Speeds things up a little bit and is going to be useful later on.

axiomatic type class 'package' for Pure (alpha version);

added "axclass.ML", structure AxClass;

added subsort, norm_sort, classes; minor internal cleanups;

replaced "logic" by logicC; added subsort, norm_sort;

replaced ext_axtab by new_axioms;

added class_triv: theory -> class -> thm (for axclasses); renamed ext_axtab to new_axioms; restored functor sig constraint :THM;

added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses); restored functor sig constraint :LOGIC;

changed syntax of use_string

changed use_string's type to string list -> unit because POLY can only handle one command per string

"Building new grammar" message is no longer displayed by empty_gram

Modified mk_meta_eq to leave meta-equlities on unchanged. Thus you may now add ==-thms to simpsets.

thy reader now initialised by init_thy_reader();

*** empty log message ***

(was Thy/read.ML) minor changes to accomodate new ThyScan and ThyParse;

*** empty log message ***

(replaces Thy/parse.ML and Thy/syntax.ML) much simpler because of new theory extension functions; theory is now built up from an arbitrary list of definable 'sections'; new axclass and instance sections;

(replaces Thy/scan.ML) scanner now based on combinators of structure Scanner; improved handling of keywords; now supports long.ids, (* (* nested *) comments *), {| verbatim text |};

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;

added const_type: sg -> typ option; stamps now stored in REVERSE order; now supports 'draft signatures' and incremental extension: is_draft, add_classes (supports axclasses), 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_name, make_draft; added const_of_class, class_of_const (for axclasses); changed the pure signature to support axclasses (added itself, TYPE); various major internal changes;

added print_sign, print_axioms: theory -> unit; replaced ["logic"] by logicS;

support for new style mixfix annotations; part of the pure syntax as mixfix (supports axclasses);

added incremental extension functions: extend_log_types, extend_type_gram, extend_const_gram, extend_consts, extend_trfuns, extend_trrules; replaced merge by merge_syntaxes; various minor internal changes;

added insort_tr, prop_tr' (for axclasses); added pure_trfuns; various minor internal changes;

replaced fix_aprop by prop_tr'; various minor internal changes;

added infix op also: 'a * ('a -> 'b) -> 'b; added set, reset, toggle: bool ref -> bool; added find_first, exists2, forall2, commas_quote, merge_rev_lists;

use_thy now uses use_string instead of creating a temporary file

added use_string: string -> unit to execute ML commands passed in a string

lookaheads are now computed faster (during the grammar is built)

extended signature SCANNER by some basic scanners and type lexicon; various minor internal changes;

added logicC: class, logicS: sort; added itselfT: typ -> typ, a_itselfT: typ (for axclasses);

added make, dest, extend_new; added exception DUPS;

fixed a bug in syntax_error, added "Building new grammar" message; automatically generated nonterminals now start with "@"

syntax_error now checks precedences when computing expected tokens

FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the simplifier can rewrite premises, it can generate the premise False."

make-all-poly, make-all-nj: restored to main directory as examples README: modified accordingly

changed implode to ^

moved 'filter is_xid' in syn_ext

syntax_error now removes duplicate tokens in its output and doesn't print the last unparsed token (i.e. EndToken)

ZF/indrule/mk_pred_typ: corrected pattern to include Abs, allowing it to handle any number of right-nested Sigmas.

renaming/removal of filenames to correct case

renaming/removal of filenames to correct case

renaming/removal of filenames to correct case

improved syntax error: now shows correct number of unparsed tokens, a special message for unexpected EOF and a list of tokens that could continue the parsed input

CTT.ML/SumE_fst,SumE_snd: tidied

Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw

final Springer version

post-CRC corrections

post-CRC corrections

post-CRC corrections

post-CRC corrections

CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw

removal of obsolete type-declaration syntax

removal of obsolete type-declaration syntax

removal of obsolete type-declaration syntax

post-CRC corrections

post-CRC corrections

post-CRC corrections

changed translation of type applications according to new grammar;

added many more filenames to FILES and EX_FILES

made a few cosmetic changes

final Springer copy

final Springer copy