Isar.toplevel_loop: separate init/welcome flag;

Sorts.class_error: produce message only (formerly msg_class_error);

tsig: removed unnecessary universal witness; Sorts.class_error: produce message only (formerly msg_class_error);

simplified handling of sorts, removed unnecessary universal witness; Envir.insert_sorts;

removed unused minimal_classes; class_error: produce message only (formerly msg_class_error); tuned;

added insert_sorts (from thm.ML);

tsig: removed unnecessary universal witness;

tuned;

removed unnecessary Goal.close_result;

replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression); pred_def: tag internal;

advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);

added is_utf8_trailer;

rep_cterm/rep_thm: no longer dereference theory_ref; removed obsolete compression;

obsolete -- Poly/ML images are maximally shared already, home-grown compression wastes space and time;

removed obsolete compress.ML

replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);

rep_cterm/rep_thm: no longer dereference theory_ref; replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);

rep_cterm/rep_thm: no longer dereference theory_ref;

use_text: explicitly print exception, which is no longer done by the new PolyML.compiler setup;

transaction/init: ensure stable theory (non-draft);

export is_draft, not draftN;

simplified isarcmd;

eliminated unused name_of, source, source_of, print', print3, three_buffersN; tuned;

eliminated unused trace, read;

eliminated unused Toplevel.print3/three_buffers;

tuned;

Isar.goal: tactical goal only;

eliminated backpatching of load_thy;

added read_const_exprs (from Pure/Isar/code_unit.ML);

export get_names (formerly names); moved pervasive theory = ThyInfo.get_theory to pure_setup.ML; removed unused pretty_theory; use OuterSyntax.load_thy instead of backpatched ThyLoad.load_thy;

ThyInfo.get_names;

ThyInfo.get_theory;

export load_thy -- no backpatching;

export subst_alias; moved read_const_exprs to Tools/code_package.ML -- avoids dependency on ThyInfo;

load thy_info.ML after outer_syntax.ML -- avoids backpatching of load_thy;

val theory = ThyInfo.get_theory;

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;

moved output_markup to xml.ML; added yxmlN mode name;

XML.output_markup;

XML.string_of, XML.parse;

replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.; added output_markup, parse_element; detect: check XY; tuned comments; tuned;

added output_markup (from Tools/isabelle_process.ML); major cleanup of signature;

replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;

tuned comments;

Added skip_mono flag to inductive definition package.

Added skip_mono flag to inductive definition package.

Added skip_mono flag and inductive_flags type.

Deleted code for axiomatic introduction of datatypes. Instead, the package now uses SkipProof.prove rather than Goal.prove to do proofs.

Removed QuickAndDirty constructor from simproc_dist datatype.

- use SkipProof.prove_global instead of Goal.prove_global - added skip_mono flag to inductive definition package

Added prove_global.

Function package no longer overwrites theorems. Some tuning.

Why XML notation?

Symbol.STX, Symbol.DEL;

Symbol.SOH;

added detect; removed auxiliary buffer_of_tree; tuned;

added some ASCII control symbols;

added Pure/General/yxml.ML;

added generalised definitions for freshness of sets of atoms and lists of atoms

tuned imports

tuned

subst_alias

improved improvements for instantiaton

canonical meet_sort operation

removed obscure "attach" feature

extended

tuned towards code generation

explicit class "eq" for operational equality

proofs adjusted to new situation in Int.thy/Presburger.thy

explicit instantiation

tuned proof

dropped wrong code lemma

moved some code lemmas for Numerals to other theories

moved some code lemmas for Numerals here

No longer imports InfiniteSet, ATP_Linkup is sufficient.

Catching up with smlnj.ML 1.47 (use_file), 1.52 (line numbers), 1.53 (forget_structure); doing some more advanced file name rewriting.

before close: Exn.capture/release;

discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn; norm_absolute: non-critical (not thread-safe!); added open_input, open_output, open_append combinators; tuned;

added add_substring; output: operate directly on stream; tuned;

discontinued File.explode_platform_path -- use plain Path.explode;

*** empty log message ***

functional theory setup -- requires linear access;

simplified print_simpset;

purely functional setup of claset/simpset/clasimpset; tuned signature;

purely functional setup of claset/simpset/clasimpset;

fixed spelling;

added exec_file; tuned;

CRITICAL: further trace levels for 1000ms and 100ms;

removed obsolete store_thm(s), cf. functional versions in pure_thy.ML; tuned;

added generic_theory transaction;

commands 'use' and 'ML' now thy_decl; removed obsolete 'ML_setup' -- superceded by 'ML';

removed obsolete use_XXX; added ml_diag;

eliminated destructive/critical theorem database; simplified store_thm(s); removed obsolete smart_store_thm(s); tuned;

certify wrt. dynamic context; functional store_thm (wrt. thread data);

added map_theory_result, map_proof_result;

certify wrt. dynamic context;

eliminated non-linear access to thy1 and thy12c;

replaced 'ML' by diagnostic 'ML_command';

updated generated file;

simplified PureThy.store_thm;

replaced 'ML_setup' by 'ML';

* Eliminated destructive theorem database. * Commands 'use' and 'ML' are now purely functional; added diagnostic 'ML_val'.

eliminated quiete_mode ref (not really needed);

eliminated quiete_mode ref (turned into proper argument);

eliminated quiete_mode ref (unused);

eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);

added forget_structure;

eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;

ml_tactic: non-critical version via proof data and thread data;

NAMED_CRITICAL;

unfold_locales now part of default tactic

import Main explicitly

dropped now superfluous ad-hoc adaption

not depends on Main any longer

accomodated to sledgehammer theory dependency requirement

only invoke interpret

updated generated file;

Context.>> : operate on Context.generic;

avoid rebinding of existing facts;

some styling

some styling

some styling

tuned proofs

tuned;

updated dependencies;

reorganized signature of ML_Context;

remove commented text

avoid ambiguity of State.state vs. JVMType.state;

declare cont_lemmas_ext as simp rules individually