1998-12-11 paulson [Fri, 11 Dec 1998 10:41:53 +0100] rev 6024
new Close_locale synatx
src/HOL/Finite.ML src/HOL/Induct/Multiset.ML src/HOL/Real/Hyperreal/Filter.ML src/HOL/UNITY/Lift.ML src/HOL/ex/LocaleGroup.ML

1998-12-11 paulson [Fri, 11 Dec 1998 10:38:51 +0100] rev 6023
deleted unclosed comment
src/HOLCF/IOA/meta_theory/LiveIOA.ML

1998-12-11 paulson [Fri, 11 Dec 1998 10:36:39 +0100] rev 6022
the + facility for locales, by Florian
src/Pure/Thy/context.ML src/Pure/Thy/thy_parse.ML src/Pure/locale.ML

1998-12-11 paulson [Fri, 11 Dec 1998 10:34:03 +0100] rev 6021
new Close_locale synatx
src/ZF/AC/AC16_WO4.ML src/ZF/AC/DC.ML

1998-12-07 paulson [Mon, 07 Dec 1998 18:26:46 +0100] rev 6020
towards handling sharing of variables
src/HOL/UNITY/PPROD.ML src/HOL/UNITY/PPROD.thy

1998-12-07 paulson [Mon, 07 Dec 1998 18:26:25 +0100] rev 6019
tidying
src/HOL/UNITY/Union.ML

1998-12-07 paulson [Mon, 07 Dec 1998 18:23:39 +0100] rev 6018
expandshort
src/HOL/UNITY/Client.ML src/HOL/UNITY/Comp.ML

1998-12-04 paulson [Fri, 04 Dec 1998 10:45:20 +0100] rev 6017
better export for nested locales
src/Pure/Thy/context.ML src/Pure/goals.ML

1998-12-04 paulson [Fri, 04 Dec 1998 10:44:02 +0100] rev 6016
new (and generalized) theorems about Sigma/Times
src/HOL/Prod.ML

1998-12-04 paulson [Fri, 04 Dec 1998 10:42:53 +0100] rev 6015
locales: assumes and defines may be empty
src/HOL/Finite.thy src/HOL/Induct/Multiset.thy src/HOL/UNITY/Lift.thy src/Pure/Thy/thy_parse.ML src/ZF/AC/DC.thy