structure Hidden = struct end;

hiding private stuff;

Symtab.foldl;

added foldl, keys;

split_paired_all.ML: turn surjective pairing into split rule;

updated

updated the MLWorks description

another little bug ;-) and minor changes in TLS.*;

little bug ;-)

added keyword 'and'

corrected Header

Addsimps [max_le_iff_conj]; Addsimps [le_min_iff_conj];

changed Super_L and Hyper_R to left and right Meta

layout

solved conflict by taking newest version;

added Clarify_tac to speed up proofs

moved a theorem

fixed comment

fixed some indenting; changed a VERY slow blast_tac to fast_tac

updated, tuned;

added Minho (Portugal);

Fixed bug (improper handling of flag flat_names).

Added quiet_mode flag.

- Changed structure of name spaces - Proofs for datatypes with unneeded parameters are working now - added additional parameter flat_names - added quiet_mode flag

tuned MLWorks options; added print_depth;

MLWorks 2.0;

Changed structure of name spaces for datatypes.

2. The simplifier now knows a little bit about nat-arithmetic.

Mods because trans_tac is now part of thge simplifier.

Mods because of: Installed trans_tac in solver of simpset().

Installed trans_tac in solver of simpset().

changed tags from 0, 1 to None, Some() to avoid special treatment of 0

parent is Main

*** empty log message ***

integer simprocs

Uses overload_1st_set to specify overloading

specifications as sets of programs

Description of new version.

New many-sorted version.

See (* FIXME zero_neq_conv *)

Nat: added zero_neq_conv List: added nth/update lemmas.

added Int.int;

PRIVATE sig parts;

length_Suc_conv is no longer given to AddIffs

new theorems

tidied

Addition of HOL/UNITY/Client

new rule

Addition of HOL/UNITY/Client

Unified treatment of type error msgs.

More pretty breaks in error msgs.

Added a few breaks in error text.

new theorem

new theorems

new guarantees laws

renamed Suc_card_Diff or something

Multisets at last!

added Induct/Multiset*

New inductive definition of `card'

polymorphic versions of nat_neq_iff and nat_neqE

Further improvement of the simplifier.

Tuned simplifier not to re-normalized already normalized terms.

tuned rm CVS;

runs test

tidying and renaming

new theorems

tidied

new files UNITY/Comp.{thy,ML}

Merges FoldSet into Finite

deleted incorrect code that set Goals.proof_timing:=false Also causes time_use_thy to set proof_timing:=true

Now prove_goalw_cterm never prints timing statistics

MLWorks demands the "op" before $

Finished proofs to end of section 5.1 of Chandy and Sanders

Join now an infix operator

simpler interface for Abel_Cancel

tidied

id <-> Id

added Real to BasisLibrary

new file Provers/Arith/abel_cancel.ML

new files Provers/Arith/abel_cancel.ML and Real/simproc.ML

tidying

white border -- disabled;

Improved definition of foldSet.

revised for new treatment of integers

new singleton_conv2

tidied

a few new lemmas.

composition theory

abstype of programs

now invokes functor

much tidying

new lemmas

better handling of literals

tidied

white space

new simproc functor

Revised version with Abelian group simprocs

handle empty name;

auto update

new function inter_term

Now id:(Acts prg) is implicit

modified proof for new simproc

many renamings and changes. Simproc for cancelling common terms in relations

New keywords

Revised wf_acc_iff and Co.

new: wfUNIVI

Package now chooses type variable names more carefully to avoid clashes with user-supplied type variable names.

minor corrections

exchanged automatic-tactics and semi-automatic-tactics added CLASET, CLASET', CLASIMPSET, CLASIMPSET'

improved indentation

rearranged SIMPSET(');

*** empty log message ***

isatool logo;

added isatool logo;

improved;

Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants

added Int to BasisLibrary

deleted illegal "op"

uses BasisLibrary for Int.min

patched obsolete code