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

new ZF/UNITY theory

*** empty log message ***

changed to full expressions with side effects

changed to full expressions with side effects

tuned;

tuned;

fix problem with user translations by making field names appear as consts;

tuned;

- Fixed bug in isomorphism proofs (caused by migration from SOME to THE) - Funs_rangeE now requires function g to be injective

Eliminated dependency of Funs_rangeE on SOME.

removed the warning from [iff]

Tweaks for 1 -> 1'

Converted 1 to 1'

1 -> 1'

Changed 1 to 1' (= Suc 0)

turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.

three new theorems

removed the warning from [iff]

removed an unsuitable default simprule

tidying and moving the theorem "choice"

new result comp_surj

numerous stylistic changes and indexing

additional revisions to chapters 1, 2

revisions and indexing

defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some dynamically, so recdef no longer needs to import Hilbert_Choice.

Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice

partial restructuring to reduce dependence on Axiom of Choice

removed reference to Ex_def

partial restructuring to reduce dependence on Axiom of Choice

tweaks and indexing

cosmetics

Final version of Florian Kammueller's examples

new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted

improved version of the Pi-theorems

PiSets moved to GroupTheory, while LocaleGroup deleted

live links

The final version of Florian Kammueller's proofs

slight improvement for iff attribute

replaced SOME by THE;

the_equality [intro];

tuned;

declare trans [trans] (*overridden in theory Calculation*);

HOL: added "The";

private "myinv" (uses "The" instead of "Eps");

replaced "Eps" by "The";

HOL_ss: the_eq_trivial, the_sym_eq_trivial;

tuned;

added "The" (definite description operator) (by Larry);

*** empty log message ***

SEDINDEX = ./isa-index;

tidying the index

tidying the index

indexing

abtract non-emptiness statements (no longer use Eps); cleaned up;

tuned;

working

oops

fixed bad error in tdxbold; also removed default indexing in \\rulename

tweaks

added\\protect

more indexing

indexing tweaks

less indexing of theorem names

indexing

contrapos_pn

index file

removed a4paper

more in the Springer style

indexing

indexing

messages, and proper treatment of footnotes

new preface

tweaks for new version

indexing and tweaks

tweak

careful changes to make its output identical to that of indexing macros

new macro file for the tutorial

separate preface and macro file

do not remove Rules and Sets TeX files

isa-index replaces ../sedindex: knows about \\isa

two Isar tactic scripts

Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential uses of this ML file (HOL/Library is in the default load path);

GroupTheory

new lemmas

better treatment of restrict (lam)

Locale-based group theory proofs

ppc-darwin;

do *not* ./configure;

#!/usr/bin/env bash;

...

the records section

the records section

for the records section

a few new and/or improved results

gave Greatest_le its proper name

resolved name clash

tidied

now more like the HOL versions, and with the Square Root example added

tidying and consolidating files

tidying and consolidating files

removed duplicate proof and small mod.

Simprocs for type "nat" no longer introduce numerals unless

Simprocs for type "nat" no longer introduce numerals unless they are already present in the expression, and in a coefficient position (i.e. as a factor of a monomial).

added NanoJava

tidied

New proof of gcd_zero after a change to Divides.ML made the old one fail

a couple of new theorems

corrected xsymbol/HTML syntax

Fixed bug in function rebuild.

new GroupTheory example, e.g. the Sylow theorem (preliminary version)

tuned

tuned Primes theory;

addition of the GREATEST quantifier

renaming of evs in the Fake rule

new material from the Sylow proof

simplified a proof using new dvd rules

moved Primes.thy from NumberTheory to Library

Removed BCV

*** empty log message ***

This is now superseded by MicroJava/BV

renamed # to ## to avoid clashing with List cons

now checks for leading meta-quantifiers and complains, instead of just raising an exception

tuned

added HOL-CTL;

tuned

examples files start from Main instead of various ZF theories

invent_names

added HOL-CTL example;

added Library/Nat_Infinity.thy and Library/Continuity.thy

added FOCUS including the One-Element Buffer by Manfred Broy

added Library/Nat_Infinity.thy and Library/Continuity.thy

added stream length, map, and filter

corrected ML names of definitions, added chain_shift

corrected ML names of definitions

improved iff_add_global, new function add_rules factoring out common behaviour

streamlined addIffs/delIffs, added warnings

replaced Sel_injective_cprod by new injective_fst_snd

added lub_range_mono and lub_range_shift

added chain_monofun

added same_fstI as safe intro rule

added injective_fst_snd

added nat_not_singleton (also to simpset)

added Least_Suc2

added list_all2_trans

added weak_coinduct_image

Allow Suc-numerals as coefficients in lin-arith formulae

corrected entry for iff attribute

extended doc for iff attribute