NEWS and CONTRIBUTORS

dded code_thm antiquotation

made SML/NJ happy

merged

merged

tuned siganture of locale.ML

tuned signature; internal code reorganisation

tuned signature; changed locale predicate name convention

changed locale predicate name convention

inductive: added fork_mono flag;

added fork_mono flag, which is usually enabled in batch-mode only; mono rule: unnamed LocalTheory.node ensures proper joining of pending proofs;

Proof.global_future_terminal_proof;

Proof.global_future_proof;

future_proof: refined version covers local_future_proof and global_future_proof; future_proof: refrain from full Variable.auto_fixes -- not all contexts in the stack are in body mode; refined is_relevant: mode check; added local/global_future_terminal_proof;

more robust propagation of errors through bulk jobs;

qed/after_qed: singleton result;

Proof.future_terminal_proof: no fork for interactive mode -- proofs need to be checked immediately here;

future_terminal_proof: no fork for interactive mode, assert_backward;

added local_theory';

merged

proper local_theory after Class.class

more parallel loading;

more parallel loading;

merged

merged.

make cont_proc handle eta-contracted terms

implement is_closed_term using Term.loose_bvar

use Thm.close_derivation instead of standard

tuned;

merged

renamed structure ParList to Par_List;

parallelized merge_data;

tuned map: reduced overhead due to bulk jobs; tuned join_results: reduced overhead for finished futures; tuned;

added is_valid; added extend: support bulk jobs; tuned;

future_terminal_proof: check Future.enabled;

merged

locale -> old_locale, new_locale -> locale

locale -> old_locale, new_locale -> locale

locale -> old_locale, new_locale -> locale

removed locale adaption layer

rearranged target theories

removed locale adaption layer

merged

misc tuning and modernization;

merged.

add lemma psize_unique; simplify some proofs

minimize imports

parallelize some internal proofs via Proof.future_terminal_proof;

added future_terminal_proof;

Isar.init;

simplified tty model -- back to plain list history, which is independent of editor model;

added is_control, is_regular, is_theory_begin;

more precise is_relevant: requires original main goal, not initial goal state; tuned future_proof: minimal modification of goal state, retain original maxidx; tuned;

tuned protect, conclude: Drule.comp_no_flatten;

added comp_no_flatten;

future proofs: back to Future.fork_pri ~1 for improved parallelism;

cancel: unique threads;

more reactive scheduler: reduced loop timeout, propagate broadcast interrupt via TaskQueue.cancel_all;

added eq_group; opaque signature match prevents accidental task/group equality; added cancel_all;

merged

separator, is_qualified

added instance for bot, top

added binding.ML

merged

merged

improved boostrap order: theory_target.ML before expression.ML

named code theorem for Fract_norm

tuned settings;

merged

removed references to OldTerm.*

tuned message_text;

removed obsolete XML mode; tuned comments; tuned;

xsymbols: use plain Symbol.output; explicit rendering of message body: print mode is always YXML, markup is only observed for singleton text (avoids overlap of inner tokens with certain status messages), test XML markup is outermost (allows Proof General font-lock); Markup.no_output;

Markup.no_output;

added output; improved encode_raw: map empty to empty; tuned;

removed unused add_substring; back to simple list implementation;

renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;

removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;

updated rendering of inner token markup;

more detailed inner token markup;

added numeral, which supercedes num, xnum, float; renamed xstr to inner_string;

renamed token markup "_xstr" to "_inner_string";

removed dead code; proper "_numeral" token markup; proper printing of arguments (higher-order numerals);

renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);

tuned;

Isar.command: plain Position.id; tuned;

added type 'a parser, simplified signature;

added type 'a parser, simplified signature; added internal_command wrapper; tuned;

added type 'a parser, simplified signature; moved properties to value_parse.ML; moved props_text to isar_syn.ML;

added props_text (from outer_parse.ML);

added Isar/value_parse.ML: Outer syntax parsers for basic ML values.

added id; tuned;

MetaSimplifier.SIMPLIFIER;

fixed assumption proof;

tuned header and description of boot files;

merged;

normalized some ML type/val aliases;

assumption/close: discontinued implicit prems;

avoid implicit use of prems;

updated generated files;

eliminated implicit use of prems; unified fact names: a, b, ab;

updated generated files;

updated type 'a lazy; proper name for type simpset;

proper import of ~~/src/HOL/ex/ReflectedFerrack;

crude adaption to intermediate class/locale version;

crude adaption to new locales;

avoid implicit prems -- tuned proofs;

avoid implicit use of prems;

Term.add_consts;

eliminated OldTerm.(add_)term_consts; eliminated polymorphic version of insert;

avoid polymorphic equality;

eliminated OldTerm.(add_)term_consts;

added canonical add_const_names, add_consts;

provide structure CharVector;

isabelle-process; provide structure Word; provide IntInf.log2;

updated sessions;

removed unused add_term_free_names;

eliminated OldTerm.add_term_free_names;

updated header;

Term.declare_typ_names, Term.declare_term_frees;

added declare_term_frees; tuned signature;

Term.declare_term_frees;

qualified Term.rename_wrt_term;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use regular Term.add_XXX etc.;

use fold_aterms directly;

use exists_Const directly;

use regular Term.add_XXX etc.;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use exists_Const directly;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;

use exists_subterm directly; moved old add_term_vars, add_term_frees etc. to structure OldTerm;

use exists_subterm directly;

use regular Term.add_vars, Term.add_frees etc.; moved old add_term_vars, add_term_frees etc. to structure OldTerm;

moved old add_term_vars, add_term_frees etc. to structure OldTerm;

use regular Term.add_vars, Term.add_frees etc.;

added old_term.ML;

Some old-style term operations.

freeze_thaw: canonical Term.add_XXX operations; varify: regular name context;

varify: regular name context;

canonical Term.add_var_names, Term.add_tvar_namesT;

canonical Term.add_var_names;

provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names; renamed add_varnames to add_var_names; removed old add_typ_ixns, add_term_tvar_ixns;

removed unused head_name_of; tuned;

merged

prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms;

New locales.

Merged.

Temporarily avoid type errors in parse phase.

More liberal consistency check for defines elements.

All logics ported to new locales.

Merged.

adapted statespace module to new locales;

More porting to new locales.

Intro_locales_tac knows about defines elements; more robust export morphism.

More porting to new locales.

Merged.

More porting to new locales

Merged.

More porting to new locales.

Prevent defines from being checked in interpretation.

Merged.

More porting to new locales.

Merged.

More porting to new locales.

More porting to new locales.

Ported HOL and HOL-Library to new locales.

Fixed legacy locale keywords (went to ZF rather than default keywords file).

Merged.

Merged.

Porting to new locales.

Theory target distinguishes old and new locales.

Merged.

Ported to new locales.

Merged; updated interpretation command in isar_syn.ML.

Merged.

Conversion of HOL-Main and ZF to new locales.

Add inherited registrations.

Refactored: evaluate specification text only in locale declarations.

Transfer theorems in print_locale.

Attributes not applied in foundational version of fact.

Transfer morphism with theory closure.

Finer-grained activation so that facts from earlier elements are available.

Transfer theorems before activation.

Use correct mode when parsing elements and conclusion.

Strict prefixes in locales expressions.

Propagate theorems to registrations.

Automated merge with ssh://ballarin@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

Equations in interpretation as goals.

Interpretation in theories: first version with equations.

Clarified comment.

Use prefix component of bindings for locale prefixes.

Missing dependency

Preserve idents (expression in sublocale).

added POSITION_PROPERTIES;

tuned;

override toString method;

Swing utilities.

merged

optional exception logging; tuned comments;

merged

pretty printer for bindings

adapted HOL source structure to distribution layout

tuned;

more markup elements;

tuned;

merged

explicit EventBus for results; removed low-level get_result/try_result;

added methods "+" and "-"; event: non-synchronized execution of handlers, based on synchronized snapshot;

Generic event bus.

eliminated fun/val confusion

merged

clean up proofs of lemma Maclaurin

disabled old jedit plugin;

more markup elements;

more markup elements;

removed duplicate sum_case used only by function package; moved projections; hide (open)

tuned NEWS; CONTRIBUTORS

renamed LexOrds.thy to Termination.thy; examples for sizechange method

tuned;

merged

refined execute, which replaces exec/exec2;

maintain initial process environment; refined execute, which replaces exec/exec2; tuned;

merged

tackling simultaneous val/fun bindings