changed comment for const_name

changed comment only;

rewritec now uses trace_thm for it's "rewrite rule from different theory" message

changed syntax of datatype declaration

replaced extend_theory by new add_* functions; changed syntax of datatype declaration

added parentheses made necessary by new constrain precedence

added parentheses made necessary by change of constrain's precedence

changed precedence of constrain to [4, 0], 3

FOL/FOL.ML/excluded_middle_tac: new

Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)

minor tidying up (ordered rewriting in Integ.ML)

modifications for cardinal arithmetic

Sara\'s perl script for renaming theory files

Addition of cardinals and order types, various tidying

Various updates and tidying

improved error msg

Improved error msg "Proved wrong thm"

parse.ML and scan.ML are now replaced by thy_parse.ML and thy_scan.ML

Franz Regensburger's changes.

atomize: borrowed HOL version, which checks for both Trueprop and == as main connective (avoids using wildcard)

problem 38 is provable

ordered rewriting applies to conditional rules as well now

replaced "foldl merge_theories" by "merge_thy_list" in base_on

added 'subclass' section; minor internal cleanups;

base_on: added 'mk_draft' arg;

(beta release)

added ext_tsig_subclass, ext_tsig_defsort; minor internal rearrangements;

added add_classrel;

replaced extend_theory;

added OldMixfix;

workaround bug in Type.expand_typ;

new datatype 'mixfix' now pervasive (old one still accesible via OldMixfix);

restored functor sig; added str_of_sort, str_of_arity, rem_sorts; minor internal cleanup;

added axclass.ML, Syntax/mixfix.ML, Thy/thy_syn.ML; removed Syntax/earley0A.ML, Thy/scan.ML, Thy/parse.ML;

added signature constraint; replaced 'also' by '|>'; added 'sigclass' section; removed pure_syntax;

removed garbage; adapted to new ThySyn (interface for 'user sections');

restored old functor name; adapted to new ThySyn;

interface for 'user sections';

replaced infix also by |>

added test for $ISABELLEBIN=source directory, to avoid isabelle/Pure being mistaken for bin/Pure

Improved error messages

reflected changes in the structure of Thy

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;