replaced Isar loop variants by generic toplevel_loop;

replaced Isar loop variants by generic toplevel_loop; eliminated obsolete get_interrupt (subsumed by crash handling);

The global Isabelle/Isar state and main read-eval-print loop.

replaced Isar.toplevel by Toplevel.program;

moved global Toplevel state to structure Isar;

made purely value-oriented, moved global state to structure Isar (cf. isar.ML); export toplevel, error_msg (formerly print_exn), transition (formerly apply); moved type isar to structure OuterSyntax; moved crashes to structure Isar;

finish: removed unnecessary Isar.init;

moved structure Isar to isar.ML; added type isar (from toplevel.ML);

Context.set_thread_data: non-critical;

added Isar/isar.ML;

improvements are strict

check validity of class target improvement

print_consts only for external specifications;

fundef_afterqed: removed unused config, added do_print flag; print_consts only for external specifications;

minimal error handling;

replaced ML by ML_val;

avoid control symbols in document (\<^fixed>);

\usepackage[english]{babel} (required for guillemots);

renamed mbind to scomp

removed syntax from monad combinators; renamed mbind to scomp

rudimentary user-syntax for terms

fix spelling

fix spelling

move lemmas from Word/BinBoolList.thy to List.thy

fixed makefiles

added missing file

tuned;

Generic conversion and tactic "atomize_elim" to convert elimination rules to the object logic

obsolete;

removed isatool expandshort; added isatool yxml;

removed obsolete AUTO_BASH feature;

removed obsolete AUTO_PERL feature;

support for YXML notation -- XML done right;

support "YXML" mode for output transfer notation; tuned;

removed abbrev for word_power. Was in the wrong direction and unused.

prefer plain ASCII here;

abs_conv: extra argument for bound variable; renamed iterated forall_conv to params_conv; added forall_conv, implies_conv, implies_concl_conv, rewr_conv;

added swap_params;

abs_conv: extra argument for bound variable;

renamed iterated forall_conv to params_conv;

instantiation replacing primitive instance plus overloaded defs; more conservative type arities

instantiation replacing primitive instance plus overloaded defs

instantiation replacing primitive instance plus overloaded defs; realpow.simps now named power_real.simps

explicit definition for "/"

explicit dummy instantiation for div

* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.

Superficial changes CVS: ----------------------------------------------------------------------

tuned

syntactic classes for bit operations

renamed app2 to map2

more new primrec

prefix for equations in primrec specifications

postprocessing of equality

parser: use plain explode, not Symbol.explode!

removed obsolete add_axiomss(_i);

renamed XML.parse_comment_whspc to XML.parse_comments;

renamed parse_comment_whspc to parse_comments; major parser cleanup -- removed junk comments;

removed yxmlN for now; moved test_markup to proof_general_emacs.ML; use efficient YXML markup internally (output, markup, message); message: issue MALFORMED MESSAGE explicitly; tuned;

moved test_markup here;

further cleanup of XML signature;

tuned comments;

further cleanup of XML signature; replaced plain_content by incremental add_content; added stream output;

output: canonical argument order (as opposed to write);

XML.string_of;