1994-06-29 clasohm 1994-06-29 added parentheses made necessary by change of constrain's precedence
1994-06-29 clasohm 1994-06-29 changed precedence of constrain to [4, 0], 3
1994-06-24 lcp 1994-06-24 FOL/FOL.ML/excluded_middle_tac: new
1994-06-24 lcp 1994-06-24 Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
1994-06-23 lcp 1994-06-23 minor tidying up (ordered rewriting in Integ.ML)
1994-06-23 lcp 1994-06-23 modifications for cardinal arithmetic
1994-06-23 lcp 1994-06-23 Sara\'s perl script for renaming theory files
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying
1994-06-21 lcp 1994-06-21 Various updates and tidying
1994-06-21 nipkow 1994-06-21 improved error msg
1994-06-20 nipkow 1994-06-20 Improved error msg "Proved wrong thm"
1994-06-20 clasohm 1994-06-20 parse.ML and scan.ML are now replaced by thy_parse.ML and thy_scan.ML
1994-06-20 nipkow 1994-06-20 Franz Regensburger's changes.
1994-06-17 lcp 1994-06-17 atomize: borrowed HOL version, which checks for both Trueprop and == as main connective (avoids using wildcard)
1994-06-17 lcp 1994-06-17 problem 38 is provable
1994-06-17 nipkow 1994-06-17 ordered rewriting applies to conditional rules as well now
1994-06-17 clasohm 1994-06-17 replaced "foldl merge_theories" by "merge_thy_list" in base_on
1994-06-16 wenzelm 1994-06-16 added 'subclass' section; minor internal cleanups;
1994-06-16 wenzelm 1994-06-16 base_on: added 'mk_draft' arg;
1994-06-16 wenzelm 1994-06-16 (beta release)
1994-06-16 wenzelm 1994-06-16 added ext_tsig_subclass, ext_tsig_defsort; minor internal rearrangements;
1994-06-16 wenzelm 1994-06-16 added add_classrel;
1994-06-09 wenzelm 1994-06-09 replaced extend_theory;
1994-06-09 wenzelm 1994-06-09 added OldMixfix;
1994-06-09 wenzelm 1994-06-09 workaround bug in Type.expand_typ;
1994-06-09 wenzelm 1994-06-09 new datatype 'mixfix' now pervasive (old one still accesible via OldMixfix);
1994-06-09 wenzelm 1994-06-09 restored functor sig; added str_of_sort, str_of_arity, rem_sorts; minor internal cleanup;
1994-06-09 wenzelm 1994-06-09 added axclass.ML, Syntax/mixfix.ML, Thy/thy_syn.ML; removed Syntax/earley0A.ML, Thy/scan.ML, Thy/parse.ML;
1994-06-01 wenzelm 1994-06-01 added signature constraint; replaced 'also' by '|>'; added 'sigclass' section; removed pure_syntax;
1994-06-01 wenzelm 1994-06-01 removed garbage; adapted to new ThySyn (interface for 'user sections');
1994-06-01 wenzelm 1994-06-01 restored old functor name; adapted to new ThySyn;
1994-06-01 wenzelm 1994-06-01 interface for 'user sections';
1994-06-01 wenzelm 1994-06-01 replaced infix also by |>
1994-06-01 lcp 1994-06-01 added test for $ISABELLEBIN=source directory, to avoid isabelle/Pure being mistaken for bin/Pure
1994-06-01 lcp 1994-06-01 Improved error messages
1994-06-01 nipkow 1994-06-01 reflected changes in the structure of Thy
1994-05-31 nipkow 1994-05-31 simpset is hidden in a functor now.
1994-05-29 nipkow 1994-05-29 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.
1994-05-26 wenzelm 1994-05-26 axiomatic type class 'package' for Pure (alpha version);
1994-05-26 wenzelm 1994-05-26 added "axclass.ML", structure AxClass;
1994-05-26 wenzelm 1994-05-26 added subsort, norm_sort, classes; minor internal cleanups;
1994-05-26 wenzelm 1994-05-26 replaced "logic" by logicC; added subsort, norm_sort;
1994-05-26 wenzelm 1994-05-26 replaced ext_axtab by new_axioms;
1994-05-26 wenzelm 1994-05-26 added class_triv: theory -> class -> thm (for axclasses); renamed ext_axtab to new_axioms; restored functor sig constraint :THM;
1994-05-26 wenzelm 1994-05-26 added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses); restored functor sig constraint :LOGIC;
1994-05-26 clasohm 1994-05-26 changed syntax of use_string
1994-05-26 clasohm 1994-05-26 changed use_string's type to string list -> unit because POLY can only handle one command per string
1994-05-26 clasohm 1994-05-26 "Building new grammar" message is no longer displayed by empty_gram
1994-05-24 nipkow 1994-05-24 Modified mk_meta_eq to leave meta-equlities on unchanged. Thus you may now add ==-thms to simpsets.
1994-05-19 wenzelm 1994-05-19 thy reader now initialised by init_thy_reader();
1994-05-19 wenzelm 1994-05-19 *** empty log message ***
1994-05-19 wenzelm 1994-05-19 (was Thy/read.ML) minor changes to accomodate new ThyScan and ThyParse;
1994-05-19 wenzelm 1994-05-19 *** empty log message ***
1994-05-19 wenzelm 1994-05-19 (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;
1994-05-19 wenzelm 1994-05-19 (replaces Thy/scan.ML) scanner now based on combinators of structure Scanner; improved handling of keywords; now supports long.ids, (* (* nested *) comments *), {| verbatim text |};
1994-05-19 wenzelm 1994-05-19 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;
1994-05-19 wenzelm 1994-05-19 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;
1994-05-19 wenzelm 1994-05-19 added print_sign, print_axioms: theory -> unit; replaced ["logic"] by logicS;
1994-05-19 wenzelm 1994-05-19 support for new style mixfix annotations; part of the pure syntax as mixfix (supports axclasses);
1994-05-19 wenzelm 1994-05-19 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;