continued

tuned

better improvement in instantiation target

*** empty log message ***

raw_loop: more graceful crash recovery;

added exception CONTEXT, indicating context of another exception; exn_message: explicit context, *not* ML_Context.get_context; toplevel_error/apply: explicit exn_context; explicit Markup.location for exn_info (cf. at_command); fixed spelling; tuned;

added location;

schedule main control: more robust interrupting of potentially running threads;

message: proper root element for XML output; token_translation: proper Output.output of content;

Proof.put_thms false;

put_facts: do_props, i.e. facts are indexed by proposition again;

put_thms: pass do_props;

tuned

dropped "include" feature of classes

some theorems named explicitly

exported suffix

fixed typo

adjusted to current implementation

instance fun :: (finite, countable) countable

tuned

added Option_ord.thy

dropped local tsigs

some steps towards a refined treatment of equality

generic improvable syntax for targets

added hithero missing overloading.ML

tuned

whitespace tuning

clarified proposition

tuned proofs

canonical order on option type

added entries

check ISABELLE_BROWSER_INFO before cd;

replaced execute by system_out;

replaced execute by system_out;

added dummy version of string_of_pid;

use "ML-Systems/universal.ML"; specific system_out;

replaced execute by system_out;

proper dependency on ML-Systems/mosml.ML;

specific system_out (MosML lacks structure Posix); dummy implementation of Posix.ProcEnv.getpid;

* system/system_out provides a robust way to invoke external shell commands, with propagation of interrupts (after Poly/ML 5.2);

system_out: threaded version does not work for 5.1;

common setup for system_out/system;

added ML-Systems/system_shell.ML;

removed obsolete THIS_IS_ISABELLE_BUILD;

obsolete (cf. ML-Systems/polyml_common.ML);

renamed polyml-old-basis.ML to polyml_old_basis.ML;

rearrangements to make latest Poly/ML the default, not old 4.x;

cleaned-up ML-Systems;

tuned comment;

removed obsolete THIS_IS_ISABELLE_BUILD feature; moved external provers further up; no HOL4_PROOFS by default;

removed obsolete THIS_IS_ISABELLE_BUILD feature: change environment after getsettings (works due to static scoping);

removed obsolete THIS_IS_ISABELLE_BUILD feature;

removed obsolete THIS_IS_ISABELLE_BUILD/MAKEBIN feature;

renamed test_markup to output_markup; added full_markup mode, with token translations;

IsabelleProcess.output_markup;

closeup: minor tuning of term traversal;

ISABELLE_LINE_EDITOR: prefer rlwrap, which passes interrupts properly;

explicit referencing of background facts;

explicit referencing of background facts;

explicit referencing of background facts;

indexing literal facts: exclude background context;

put_thms: do not index facts here (affects prems/this/calculation in particular);

explicit referencing of background facts;

HOL/Library/RBT.thy;

NEWS: RBTs, renamings in ZF

Use conversions instead of simplifier. tuned

added new example

tuned

continued localization

new theory of red-black trees, an efficient implementation of finite maps.

Generalized Zorn and added well-ordering theorem

tuned ML code, more antiquotations;

misc cleanup of embedded ML code; use more antiquotations; tuned;

added @{const} antiquotation;

use more antiquotations;

unused_thms: print via official context (ProofContext.pretty_fact), not just the theory certificate (Display.pretty_thm); tuned;

Added function for finding unused theorems.

Added unused_thms command.

import all 'special code' types

added code generator setup

Transitive_Closure: induct and cases rules now declare proper case_names;

Transitive_Closure: induct and cases rules now declare proper case_names; tuned;

rtranclp_induct, tranclp_induct: added case_names; tuned proofs;

tuned

removed legacy ML bindings;

tuned syntax declaration;

wf_trancl: structured proof; tuned proofs; removed legacy ML bindings;

rtranclE, tranclE: tuned statement, added case_names;

renamed ListSpace to ListVector;

added HOL-Library;

more precise handling of "group" for termination;

added theories for imperative HOL

added theory for countable types

added theory for reflected types

proper merge of base sorts

Renamed ListSpace to ListVector

Fixed dependency on Dense_Linear_Order

removed some debugging output from trace

Loads Dense_Linear_Order (needed dlo_simps)

Fixed dependencies for proofs -- ferrack needed

Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.

fixed dependencies

Removed theorems from default simpset

Fixed proofs

Loads Dense_Linear_Order.thy

loads Tools/Qelim/qelim.ML

HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated

Installation of Quantifier elimination for ordered fields moved to Library/Dense_Linear_Order.thy

other UNIV lemmas

some more primrec

class itself works around a problem with class interpretation in class finite

moved some set lemmas from Set.thy here

tuned heading

char and nibble are finite

moved some set lemmas to Set.thy

tuned proofs

tuned document; tuned proofs;

tuned document;

Added useful general lemmas from the work with the HeapMonad

some steps towards automated generators

operation collapse

Zero/Suc recursion combinator for type index

added accidental omissions

thm_deps: sort result;

tuned msg;

fixed ChangeLog.gz path;

fixed document;

welcome: actually check for ChangeLog.gz; tuned structure Distribution;

tuned structure Distribution;

implicit use of LocalTheory.group etc.;

maintain group in lthy data, implicit use in operations; tuned signature; added group_position_of;

tuned;

LocalTheory.set_group for user command;

inductive package: simplified group handling;

Added dependency of Library on Pocklington.thy

Pocklington's Primality criterion

More primality theorems

A library for univariate polynomials -- generalizes old Hyperreal/Poly.thy from reals to locales

A proof a the fundamental theorem of algebra

Uses Univ_Poly.thy

Does not import Poly anymore

Includes the derivates of polynomials -- reals specific content of Poly

Two simple theorems about cmod moved to Complex.thy

Now imports Funamental_Theorem_Algebra

Added trivial theorems aboud cmod

Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed

removed dead code; some cleanup

non-operative code antiquotation

non-operative code antiquotation

added further interface for reading constants

added first version of datatype antiquotation

moved refute_tac to linarith.ML

more elaborate structure Distribution (filled-in by makedist);

keep ChangeLog.gz within distribution; more elaborate structure Distribution (filled-in by makedist);

removed junk;

moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas

moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and added some

removed NBE;

removed ex/NBE.thy;

fix proofs involving ile_def

tuned structures in arith_data.ML

using only an relation predicate to construct div and mod

now in AFP

added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);

removed General/system_process.ML (back to multithreaded version);

replaced setpgrp by more elaborate setsid;

slightly tuned

Yet another proof of False, this time using the strong case analysis rule.

tuned

system.pl - invoke shell command line (with robust signal handling);

updated

added eqvt-flag to subseteq-lemma

proved linorder and wellorder class instances

added get_parent (for AWE); tuned;

added perl wrapper for robust signal handling;

New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1

removed spurious PolyML.makestring;

replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;

removed managed_process (cf. General/shell_process.ML); replaced ignore/raise_interrupt by more flexible (un)interruptible combinators; tuned timeLimit: sleep already interruptible by default; schedule: restore attributes of body, instead of forcing interruptible execution;

removed managed_process (cf. General/shell_process.ML);

exn_message: added TimeLimit.TimeOut; replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;

export deny_secure;

setmp: uninterruptible;

System shell processes, with static input/output and propagation of interrupts.

added General/system_process.ML;

added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps

added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps

support for managed external processes;

more lemmas

<= and < on nat no longer depend on wellfounded relations

moved *_reorient lemmas here

tuned names;