src/HOL/Bali/Basis.thy
2011-10-15 wenzelm 2011-10-15 misc tuning and modernization;
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-08-02 krauss 2011-08-02 eliminated obsolete recdef/wfrec related declarations
2010-07-26 wenzelm 2010-07-26 modernized/unified some specifications;
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-03 wenzelm 2010-03-03 cleanup type translations;
2010-03-01 haftmann 2010-03-01 merged
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-24 wenzelm 2010-02-24 modernized syntax declarations, and make them actually work with authentic syntax;
2010-02-10 wenzelm 2010-02-10 modernized syntax translations, using mostly abbreviation/notation; minor tuning;
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-11-27 haftmann 2009-11-27 Inl and Inr now with authentic syntax
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-08-14 krauss 2009-08-14 reverted accidential corruption of superscripts introduced in a508148f7c25
2009-08-13 paulson 2009-08-13 Removal of redundant settings of unification trace and search bounds.
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to Option.map
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-16 wenzelm 2008-06-16 sum3_instantiate: proper context;
2008-06-11 wenzelm 2008-06-11 Drule.read_instantiate;
2008-03-20 haftmann 2008-03-20 tuned proof
2007-08-09 haftmann 2007-08-09 re-eliminated Option.thy
2007-08-07 wenzelm 2007-08-07 turned Unify flags into configuration options (global only);
2007-08-07 haftmann 2007-08-07 split off theory Option for benefit of code generator
2007-07-29 wenzelm 2007-07-29 replaced make_imp by rev_mp;
2007-07-28 wenzelm 2007-07-28 tuned ML/simproc declarations;
2007-04-24 berghofe 2007-04-24 sum_case is now authentic.
2007-04-11 haftmann 2007-04-11 tuned
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-11-12 wenzelm 2006-11-12 removed dead code;
2006-03-23 nipkow 2006-03-23 Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.
2006-01-04 nipkow 2006-01-04 Reversed Larry's option/iff change.
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-10-07 wenzelm 2005-10-07 removed obsolete dummy_pat_tr;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-31 wenzelm 2005-05-31 tuned;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2003-03-17 nipkow 2003-03-17 just a few mods to a few thms
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-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-02-22 schirmer 2002-02-22 Added check for field/method access to operational semantics and proved the acesses valid.
2002-02-21 wenzelm 2002-02-21 removed theory Option;
2002-02-15 wenzelm 2002-02-15 replaced nodups by distinct;
2002-01-28 wenzelm 2002-01-28 tuned;
2002-01-28 wenzelm 2002-01-28 GPLed;
2002-01-28 wenzelm 2002-01-28 tuned header;
2002-01-28 schirmer 2002-01-28 Isabelle/Bali sources;