unsymbolize;

renamed "()" to Unity;

HOLogic.unit;

made unit type local;

tuned:

renamed "()" to Unity, made local;

added surjE;

prepared for Isabelle2001;

renamed real_of_nat_eq_cancel to real_of_nat_inject, and declared as iff rule;

updated;

renamed real_of_int_eq_iff to real_of_int_inject;

document setup;

new-style theory;

Square roots of primes are irrational;

AddXIs [dvdI]; AddXEs [dvdE]; added dvd_mult_div_cancel;

tuned;

tuned;

tuned;

AddXEs [UnI1, UnI2];

AddXEs [disjI1, disjI2];

ex/Hilbert_Classical.thy ex/document/root.tex;

tuned;

document setup;

derive tertium-non-datur by means of Hilbert's choice operator;

obsolete;

updated;

-v option;

verbose option;

use_dir: verbose option;

removed option -d (now standard behaviour); added option -q; include notes;

option -v;

activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;

updated;

tuned order;

bold symbols;

tuned;

turn bullet into bold cdot (looks much better in printed output);

use darkblue for all links;

updated;

updated;

*** empty log message ***

tuned;

Minor improvements, added Example

tuned;

Fixed proof term bug in permute_prems.

result_error_default: include msg;

*** empty log message ***

marginally improved comments

corrected antiquotations in comment

simplified vnam/vname, introduced fname, improved comments

tuned usage;

print_state: subgoals;

export pretty_goals;

result_error_default: output *single* error message;

tuned;

ISABELLE_INTERFACE=none by default (cannot expect X11 everywhere);

* system: support Poly/ML 4.1.1 (large heaps); * system: smart selection of Isabelle process versus Isabelle interface, accomodates case-insensitive file systems (e.g. HFS+);

smart selection of isabelle-process versus isabelle-interface;

renamed "antecedent" case to "rule_context";

*** empty log message ***

*** empty log message ***

tuned;

final proofs := 0;

HOL-Real-Hyperreal made a plain session (no longer an image);

renamed `keep_derivs' to `proofs', and made an integer;

* Proof General keywords specification is now part of the Isabelle distribution (see etc/isar-keywords.el);

proper use of invent_names;

fixed header;

tuned headers;

keyword classification tables for Isabelle/Isar Proof General (generated by ProofGeneral.write_keywords from Isabelle/HOLCF/IOA);

New code generators for HOL.

Initial revision of tools for proof terms.

Added new option for setting level of detail for proof objects.

Proof of True_implies_equals is stored with "open" derivation to facilitate simplification of proof terms.

Added code generator setup.

Added new files for code generator.

Renamed functions % and %% to avoid clash with syntax for proof terms.

Adapted to new proof terms.

Exported ml_reserved.

Made consts list operations a bit faster.

Added new argument to use_dir for derivation kind.

Removed tag_assumption.

Tuned naming of theorems.

Added functions for printing primitive proof terms.

Tuned function extend_lexicon.

Initial revision of tools for proof terms.

Now obsolete; replaced by LF style proof terms.

Initial version of generic code generator.

New implementation of LF style proof terms.

Replaced old derivations by proof terms.

Tidied function SELECT_GOAL.

Added equality axioms and initialization of proof term package.

Added setup for code generator.

Added function unique_strings.

- exported SAME exception - exported functions for normalizing types

Some basic rules are now stored with "open" derivations, to facilitate simplification of proof terms.

Added new files for proof terms.

generated by Session.name;

export name;

cosmetics

removed imname, uncurried Meth

avoid ML bindings;

Implemented indentation schema for conditional rewrite trace.

Traced depth of conditional rewriting

tuned error message;

prefer immediate monos; tuned;

support for absolute namespace entry paths;

Updated proofs to take advantage of additional theorems proved by "typedef"

removed obsolete "arities";

tuned;

corrected initialization of locals, streamlined Impl

corrected semantics of [iff] concerning rules with premises

replaced 1 by 1'

revisions and indexing

added pair_imageI (also as intro rule)

renamed addaltern to addafter, addSaltern to addSafter

added constify_ast_tr;

field_name_ast_tr superceded by constify_ast_tr in Pure;

_constify;

constify numeral tokens in order to allow translations;

* HOL: syntax translations now work properly with numerals and records expressions;

layout, subscripts

[ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120";

polyml-4.1.1;

Hilbert_Choice is needed only in Main itself

Main is the proper parent of IOA

get it working again using Hilbert_Choice

Getting it working again with 1' instead of 1