src/Pure/Isar/context_rules.ML
2013-03-29 wenzelm 2013-03-29 Pretty.item markup for improved readability of lists of items;
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-01 wenzelm 2009-11-01 tuned signature;
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup; replaced add_args by add parser;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-01-26 wenzelm 2008-01-26 tuned attribute syntax -- no need for eta-expansion;
2007-06-03 wenzelm 2007-06-03 tuned Tactic signature;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic;
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-08 haftmann 2006-02-08 introduced gen_distinct in place of distinct
2006-02-03 wenzelm 2006-02-03 canonical member/insert/merge;
2006-01-31 wenzelm 2006-01-31 tuned;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-15 wenzelm 2006-01-15 export add_args; tuned;
2006-01-13 wenzelm 2006-01-13 tuned;
2006-01-10 wenzelm 2006-01-10 generic data and attributes; tuned;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-10-28 haftmann 2005-10-28 cleaned up nth, nth_update, nth_map and nth_string functions
2005-09-20 wenzelm 2005-09-20 tuned;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-13 wenzelm 2005-09-13 tuned;
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-06-21 wenzelm 2005-06-21 tuned;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
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
2004-03-19 paulson 2004-03-19 Removing the datatype declaration of "order" allows the standard General.order to be used. Thus we can use Int.compare and String.compare instead of the slower home-grown versions.
2002-07-16 wenzelm 2002-07-16 module now right after ProofContext (for locales);
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2002-01-17 wenzelm 2002-01-17 Thm.prop_of;
2001-12-06 wenzelm 2001-12-06 fixed dest atts;
2001-12-06 wenzelm 2001-12-06 tuned;
2001-12-05 wenzelm 2001-12-05 export low-level addXXs; find_rules interface;
2001-12-03 wenzelm 2001-12-03 renamed rule_context.ML to context_rules.ML;