1994-07-01 ago clasohm replaced extend_theory by new add_* functions;
1994-06-29 ago clasohm added parentheses made necessary by new constrain precedence
1994-06-29 ago clasohm added parentheses made necessary by change of constrain's precedence
1994-06-29 ago clasohm changed precedence of constrain to [4, 0], 3
1994-06-24 ago lcp FOL/FOL.ML/excluded_middle_tac: new
1994-06-24 ago lcp Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
1994-06-23 ago lcp minor tidying up (ordered rewriting in Integ.ML)
1994-06-23 ago lcp modifications for cardinal arithmetic
1994-06-23 ago lcp Sara\'s perl script for renaming theory files
1994-06-21 ago lcp Addition of cardinals and order types, various tidying
1994-06-21 ago lcp Various updates and tidying
1994-06-21 ago nipkow improved error msg
1994-06-20 ago nipkow Improved error msg "Proved wrong thm"
1994-06-20 ago clasohm parse.ML and scan.ML are now replaced by thy_parse.ML and thy_scan.ML
1994-06-20 ago nipkow Franz Regensburger's changes.
1994-06-17 ago lcp atomize: borrowed HOL version, which checks for both Trueprop
1994-06-17 ago lcp problem 38 is provable
1994-06-17 ago nipkow ordered rewriting applies to conditional rules as well now
1994-06-17 ago clasohm replaced "foldl merge_theories" by "merge_thy_list" in base_on
1994-06-16 ago wenzelm added 'subclass' section;
1994-06-16 ago wenzelm base_on: added 'mk_draft' arg;
1994-06-16 ago wenzelm (beta release)
1994-06-16 ago wenzelm added ext_tsig_subclass, ext_tsig_defsort;
1994-06-16 ago wenzelm added add_classrel;
1994-06-09 ago wenzelm replaced extend_theory;
1994-06-09 ago wenzelm added OldMixfix;
1994-06-09 ago wenzelm workaround bug in Type.expand_typ;
1994-06-09 ago wenzelm new datatype 'mixfix' now pervasive (old one still accesible via OldMixfix);
1994-06-09 ago wenzelm restored functor sig;
1994-06-09 ago wenzelm added axclass.ML, Syntax/mixfix.ML, Thy/thy_syn.ML;
1994-06-01 ago wenzelm added signature constraint;
1994-06-01 ago wenzelm removed garbage;
1994-06-01 ago wenzelm restored old functor name;
1994-06-01 ago wenzelm interface for 'user sections';
1994-06-01 ago wenzelm replaced infix also by |>
1994-06-01 ago lcp added test for $ISABELLEBIN=source directory, to
1994-06-01 ago lcp Improved error messages
1994-06-01 ago nipkow reflected changes in the structure of Thy
1994-05-31 ago nipkow simpset is hidden in a functor now.
1994-05-29 ago nipkow Internale optimization of the simplifier: in case a subterm stays unchanged,
1994-05-26 ago wenzelm axiomatic type class 'package' for Pure (alpha version);
1994-05-26 ago wenzelm added "axclass.ML", structure AxClass;
1994-05-26 ago wenzelm added subsort, norm_sort, classes;
1994-05-26 ago wenzelm replaced "logic" by logicC;
1994-05-26 ago wenzelm replaced ext_axtab by new_axioms;
1994-05-26 ago wenzelm added class_triv: theory -> class -> thm (for axclasses);
1994-05-26 ago wenzelm added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
1994-05-26 ago clasohm changed syntax of use_string
1994-05-26 ago clasohm changed use_string's type to string list -> unit because POLY can only
1994-05-26 ago clasohm "Building new grammar" message is no longer displayed by empty_gram
1994-05-24 ago nipkow Modified mk_meta_eq to leave meta-equlities on unchanged.
1994-05-19 ago wenzelm thy reader now initialised by init_thy_reader();
1994-05-19 ago wenzelm *** empty log message ***
1994-05-19 ago wenzelm (was Thy/read.ML)
1994-05-19 ago wenzelm *** empty log message ***
1994-05-19 ago wenzelm (replaces Thy/parse.ML and Thy/syntax.ML)
1994-05-19 ago wenzelm (replaces Thy/scan.ML)
1994-05-19 ago wenzelm new datatype theory, supports 'draft theories' and incremental extension:
1994-05-19 ago wenzelm added const_type: sg -> typ option;
1994-05-19 ago wenzelm added print_sign, print_axioms: theory -> unit;