1997-01-17 paulson 1997-01-17 Now with Andy Gordon's treatment of freshness to replace newN/K
1997-01-17 paulson 1997-01-17 Deleted the redundant theorem subset_empty_iff (subset_empty exists already)
1997-01-17 paulson 1997-01-17 Added the prlim command
1997-01-17 paulson 1997-01-17 New miniscoping rules for the bounded quantifiers and UN/INT operators
1997-01-17 nipkow 1997-01-17 Got rid of Alls in List. Added Ball_insert and Ball_Un in equalities.ML.
1997-01-17 nipkow 1997-01-17 Got rid of Alls in favour of !x:set_of_list
1997-01-16 wenzelm 1997-01-16 binary oprations and relations; nat;
1997-01-16 wenzelm 1997-01-16 added termless parameter; added simplification procedures;
1997-01-16 wenzelm 1997-01-16 added term order;
1997-01-13 wenzelm 1997-01-13 improved error msg;
1997-01-13 wenzelm 1997-01-13 added datatype order;
1997-01-13 wenzelm 1997-01-13 added -? option;
1997-01-13 wenzelm 1997-01-13 replaced unit refs by 'stamp';
1997-01-10 wenzelm 1997-01-10 cleaned up (real changes next time);
1997-01-09 wenzelm 1997-01-09 make all Isabelle systems afresh;
1997-01-09 wenzelm 1997-01-09 *** empty log message ***
1997-01-09 wenzelm 1997-01-09 IsaMakefile for ZF;
1997-01-09 paulson 1997-01-09 Tidying of proofs. New theorems are enterred immediately into the relevant clasets or simpsets.
1997-01-09 paulson 1997-01-09 New theorem add_leE
1997-01-09 paulson 1997-01-09 New treatment of nonce creation
1997-01-09 paulson 1997-01-09 Removal of needless "addIs [equality]", etc.
1997-01-08 paulson 1997-01-08 New discussion of implicit simpsets & clasets
1997-01-08 wenzelm 1997-01-08 IsaMakefile for HOLCF;
1997-01-08 paulson 1997-01-08 Removal of sum_cs and eq_cs
1997-01-08 wenzelm 1997-01-08 IsaMakefile for Sequents;
1997-01-08 wenzelm 1997-01-08 IsaMakefile for CTT;
1997-01-08 wenzelm 1997-01-08 IsaMakefile for FOLP;
1997-01-08 wenzelm 1997-01-08 IsaMakefile for CCL;
1997-01-08 wenzelm 1997-01-08 IsaMakefile for LCF;
1997-01-08 wenzelm 1997-01-08 IsaMakefile for Cube;
1997-01-08 paulson 1997-01-08 Removed some (not all!) uses of FOL_cs
1997-01-07 paulson 1997-01-07 Simplification of some proofs, especially by eliminating the equality in RA2
1997-01-07 paulson 1997-01-07 Incorporation of HPair into Message
1997-01-07 paulson 1997-01-07 Default rewrite rules for quantification over Collect(A,P)
1997-01-07 paulson 1997-01-07 Default rewrite rules for quantification over Collect(A,P)
1997-01-07 paulson 1997-01-07 Now uses HPair
1997-01-07 paulson 1997-01-07 Tidied up the unicity proofs
1997-01-07 paulson 1997-01-07 Updated account of implicit simpsets and clasets
1997-01-07 wenzelm 1997-01-07 added ISABELLE, ISATOOL;
1997-01-07 wenzelm 1997-01-07 testdir: use dir without committing into database;
1997-01-07 wenzelm 1997-01-07 added dvi viewer alternative;
1997-01-07 wenzelm 1997-01-07 fixed cmp -s option;
1997-01-07 wenzelm 1997-01-07 minor tuning;
1997-01-07 wenzelm 1997-01-07 minor tuning; added Auth/Recur;
1997-01-07 wenzelm 1997-01-07 minor tuning; added thy_data.ML cladata.ML;
1997-01-06 wenzelm 1997-01-06 added stamp util;
1997-01-03 paulson 1997-01-03 A definition of "print", unfortunately overridden by each "open PolyML"
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1997-01-03 paulson 1997-01-03 Added TFL
1997-01-03 paulson 1997-01-03 Conversion to Basis Library (using prs instead of output)
1996-12-20 wenzelm 1996-12-20 changed xterm geometry;
1996-12-20 oheimb 1996-12-20 removed test
1996-12-20 oheimb 1996-12-20 testing...
1996-12-20 sandnerr 1996-12-20 testing cvs merge algorithm, 2nd
1996-12-20 oheimb 1996-12-20 testing...
1996-12-20 sandnerr 1996-12-20 testing cvs merge algorithm
1996-12-20 oheimb 1996-12-20 testing...
1996-12-20 oheimb 1996-12-20 testing: last line w/o nl
1996-12-20 oheimb 1996-12-20 testing: last line w/o nl
1996-12-20 oheimb 1996-12-20 testing...