isabelle: Changelog

Mercurial isabelle / changelog

summary | shortlog | changelog | graph | tags | branches | files | gz

1997-05-27 wenzelm [Tue, 27 May 1997 15:45:07 +0200] rev 3362 Isabelle94-8

NJ 1.09.2x as factory default!

1997-05-27 mueller [Tue, 27 May 1997 15:07:02 +0200] rev 3361

Last changes for new release 94-8

src/HOLCF/IOA/meta_theory/CompoTraces.ML src/HOLCF/IOA/meta_theory/Seq.ML src/HOLCF/IOA/meta_theory/Sequence.ML src/HOLCF/IOA/meta_theory/ShortExecutions.ML src/HOLCF/IOA/meta_theory/ShortExecutions.thy src/HOLCF/IOA/meta_theory/Traces.ML

1997-05-27 wenzelm [Tue, 27 May 1997 14:38:49 +0200] rev 3360

added 1.09.28 note;

1997-05-27 paulson [Tue, 27 May 1997 13:26:42 +0200] rev 3359

New theorems suggested by Florian Kammueller

src/HOL/ex/Primes.ML

1997-05-27 paulson [Tue, 27 May 1997 13:26:11 +0200] rev 3358

Restoration of the two "bypassed" theorems Union_quotient and quotient_disj

src/HOL/Integ/Equiv.ML

1997-05-27 paulson [Tue, 27 May 1997 13:25:00 +0200] rev 3357

Removal of card_insert_disjoint, which is now a default rewrite rule

src/HOL/Induct/Mutil.ML

1997-05-27 paulson [Tue, 27 May 1997 13:24:15 +0200] rev 3356

New theorem disjoint_eq_subset_Compl

src/HOL/equalities.ML

1997-05-27 paulson [Tue, 27 May 1997 13:23:53 +0200] rev 3355

New theorem le_Suc_eq

src/HOL/NatDef.ML

1997-05-27 paulson [Tue, 27 May 1997 13:23:27 +0200] rev 3354

Removal of mask.sig and mask.sml

src/HOL/IsaMakefile

1997-05-27 paulson [Tue, 27 May 1997 13:22:30 +0200] rev 3353

Removal of module Mask and datatype binding with its constructor |->

TFL/mask.sig TFL/mask.sml TFL/rules.new.sml TFL/rules.sig TFL/sys.sml TFL/tfl.sml TFL/thry.sig TFL/thry.sml TFL/usyntax.sig TFL/usyntax.sml

isabelle