Changed bstring argument to xstring.

*** empty log message ***

Added optional theorem names for the constant definitions added during specification.

Added package for definition by specification.

tidying

Fixing a simproc bug

tidying

Some new thm (ex_map_conv?)

use Library.Some/None instead of just Some/None in generated quickcheck code

Added keywords for random testing.

Restored old (tail recursive!) version of repeat.

Exported function goal_params.

Added several functions for producing random numbers.

Added functions for random testing.

Added generator for test case generators.

mk_int now produces specific constants for 0 and 1.

- Installed specific code generator for equality enforcing that arguments do not have function types, which would result in an error message during compilation. - Added test case generators for basic types.

added upd_fst, upd_snd, some thms

added map_image, restrict_map, some thms

added fold_red, o2l, postfix, some thms

added rev_ballE

re-introduced sort constraints on LHS

corrected markup text

Changed many Intersection rules from i:I to I~=0 to avoid introducing a new variable

~= to neq

converting more theories to Isar scripts, and tidying

Conversion of ZF/UNITY/{FP,Union} to Isar script. Introduction of X-symbols to the ML files.

A patch by david aspinall

Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been compiled without proof objects.

converted UNITY/Comp/{AllocImpl,Client} to Isar scripts

converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)

Conversion of UNITY/Comp/Priority.thy to a linear Isar script

Type antiquotations do not use the bracket syntax by default any longer.

moved some lemmas here from ZF

Removal of UNITY/UNITYMisc, moving its theorems elsewhere. Conversion of UNITY/State to Isar format.;

Added DOCTYPE and Content-type to HTML documents.

Moved function for renaming bound variables to Pure/drule.ML

Added functions for renaming bound variables.

Added split_paired_All rule for splitting variables bound by object-level universal quantifiers.

- record_split_tac now also works for object-level universal quantifier - bound variables in split rule now have nicer names - added new simproc record_eq_simproc which prevents simplifier from choosing the "wrong" equality rule

integrated optimizations by Sebastian Skalberg, produces less garbage, is faster and clearer

Conversion of theory UNITY to Isar script

Conversion of AllocBase to new-style

*** empty log message ***

*** empty log message ***

Conversion of "Merge" to Isar format

Conversion of UNITY/Distributor to Isar script. General tidy-up.

Converting ZF/UNITY to Isar

Added new theories StrongNorm and WeakNorm to Lambda example.

Bibliography file with paper by Matthes and Joachimski.

Added bibliography.

Added new theories WeakNorm and StrongNorm.

Added lift_map and subst_map.

Nicer syntax for beta reduction.

Moved strong normalization proof to StrongNorm.thy

New proof of weak normalization with program extraction.

*** empty log message ***

conversion of ClientImpl to Isar script

Adding the theory UNITY/AllocImpl.thy, with supporting lemmas

inserted TUM in other places

added TUM

x-symbols (mostly)

remove -p option, separate setting available

Further tweaks of ZF/UNITY

getting ZF/UNITY working again

Introduction of the theories UNITY/Merge, UNITY/ClientImpl

some new ZF/UNITY material from Sidi Ehmety

examples now use Complex_Main

new theorem

Added term_of function for product type.

Added pair_const.

removed redundant line

updating ZF-UNITY with Sidi's new material

Introduced distinction wf_prog vs. ws_prog

set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible) switched off by default

fixed

make it possible to switch off proof objects for HOL image

make it possible to switch off proof objects

be less verbose about simplification depth

fix typo

attach log files

more cleanup

fix mime stuff

attach log files

support text file attachments

Added a few lemmas about map_le

give tests time to copy settings

Added Bali to test

Adapted to changes in Map.thy

use proof objects for HOL by default

eparation logic - a beginning.

*** empty log message ***

*** empty log message ***

*** empty log message ***

HOL-Real -> HOL-Complex

*** empty log message ***

tweaked

*** empty log message ***

oops

different colors for new release

Improved entry on Algebra.

no separate x-symbol package

Isabelle2002

removed new jersey mirror

done

moved % comments out of ttboxes

be nice on sunbroy2

MicroJava LBV

Bali

removed references to KDE versions (works for any).

Program extraction framework.

smlnj link update, x-symbol/PG update

some information for Constructible

some information for Complex

updated text

makefiles for latex runs

defer latex run to Makefile (not IsaMakefile)

added isar-overview

added IsarOverview

IsarOverview moved one level up

Added new function eta_long.

- Added split_min and split_max to preprocessor - Moved eta_long to Pure/pattern.ML

*** empty log message ***

NEWS updated for HOL-Algebra.

tuned

only make development snapshots for successful tests

fixes

var/run -> var/running