2010-03-03 wenzelm 2010-03-03 cleanup type translations;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-23 haftmann 2010-02-23 dropped axclass
2010-02-10 wenzelm 2010-02-10 modernized syntax translations, using mostly abbreviation/notation; minor tuning;
2010-01-30 berghofe 2010-01-30 Adapted to changes in cases method.
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-25 Thomas Sewell 2009-09-25 Avoid record-inner constants in polymorphic definitions in Bali The Bali package needs to insert a record extension into a type class and define an associated polymorphic constant. There is no elegant way to do this. The existing approach was to insert every record extension into the type class, defining the polymorphic constant at each layer using inner operations created by the record package. Some of those operations have been removed. They can be replaced by use of record_name.extend if necessary, but we can also sidestep this altogether. The simpler approach here is to use defs(overloaded) once to provide a single definition for the composition of all the type constructors, which seems to be permitted. This gets us exactly the fact we need, with the cost that some types that were admitted to the type class have no definition for the constant at all.
2009-07-22 haftmann 2009-07-22 set intersection and union now named inter and union
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to
2007-10-22 wenzelm 2007-10-22 abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
2007-07-29 wenzelm 2007-07-29 replaced make_imp by rev_mp;
2007-07-11 berghofe 2007-07-11 Renamed inductive2 to inductive.
2007-03-09 haftmann 2007-03-09 resolved name clashes
2006-12-11 berghofe 2006-12-11 Adapted to new inductive definition package.
2006-05-05 krauss 2006-05-05 First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-06 schirmer 2004-05-06 tuned HOL/record package; enabled record_upd_simproc by default.
2004-05-03 schirmer 2004-05-03 reimplementation of HOL records; only one type is created for each record extension, instead of one type for each field. See NEWS.
2003-05-14 schirmer 2003-05-14 Adapted to changes in Map.thy
2003-05-14 nipkow 2003-05-14 *** empty log message ***
2002-10-31 schirmer 2002-10-31 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-02-27 schirmer 2002-02-27 Cleaning up the definition of static overriding.
2002-02-25 wenzelm 2002-02-25 clarified syntax of ``long'' statements: fixes/assumes/shows;
2002-02-22 schirmer 2002-02-22 Added check for field/method access to operational semantics and proved the acesses valid.
2002-01-28 wenzelm 2002-01-28 tuned;
2002-01-28 schirmer 2002-01-28 Isabelle/Bali sources;