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;