src/HOL/Bali/Basis.thy
21 months ago haftmann 2017-10-08 replaced recdef were easy to replace
23 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-02-23 nipkow 2016-02-23 more canonical names
2016-01-02 wenzelm 2016-01-02 isabelle update_cartouches -c -t;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-03-19 wenzelm 2015-03-19 more position information;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-18 blanchet 2014-09-18 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-08-18 blanchet 2014-08-18 reordered some (co)datatype property names for more consistency
2014-02-16 blanchet 2014-02-16 folded 'Option.set' into BNF-generated 'set_option'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-26 wenzelm 2014-01-26 tuned signature;
2014-01-25 wenzelm 2014-01-25 explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
2013-05-16 wenzelm 2013-05-16 tuned signature -- depend on context by default;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-02-28 wenzelm 2013-02-28 marginalized historic strip_tac;
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