src/FOLP/IFOLP.thy
2016-01-11 wenzelm 2016-01-11 eliminated old defs;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-06-22 wenzelm 2015-06-22 support 'when' statement, which corresponds to 'presume';
2015-02-11 wenzelm 2015-02-11 proper context and method setup;
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-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-03-18 wenzelm 2014-03-18 tuned signature -- rearranged modules;
2014-02-10 wenzelm 2014-02-10 prefer vacuous definitional type classes over axiomatic ones;
2013-05-30 wenzelm 2013-05-30 standardized aliases;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-20 wenzelm 2011-11-20 tuned;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-05-14 wenzelm 2011-05-14 modernized functor names; tuned;
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
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-08-27 wenzelm 2010-08-27 proper configuration option "show_proofs"; modernized syntax translation;
2010-08-18 haftmann 2010-08-18 deglobalization
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-04-23 wenzelm 2010-04-23 mark schematic statements explicitly;
2010-02-15 wenzelm 2010-02-15 eliminated unnamed infixes;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax};
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-01-02 wenzelm 2009-01-02 fixed assumption proof;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-06-11 wenzelm 2008-06-11 changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;
2008-06-11 wenzelm 2008-06-11 tuned comments;
2008-05-18 wenzelm 2008-05-18 setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-03-18 wenzelm 2008-03-18 converted legacy ML scripts;
2005-09-18 wenzelm 2005-09-18 converted to Isar theory format;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
1999-04-26 paulson 1999-04-26 fixed a bug many years old in rule plusEC
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-03-04 paulson 1997-03-04 Removed needless quotes
1996-02-05 clasohm 1996-02-05 expanded tabs
1995-06-21 clasohm 1995-06-21 removed \...\ inside strings
1995-06-02 lcp 1995-06-02 Corrected comments in headers
1994-10-21 lcp 1994-10-21 FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities. Now proof objects have high precedences. Eliminates ambiguity in a=b:P being parsed as (a=b):P.
1994-03-17 lcp 1994-03-17 new type declaration syntax instead of numbers
1993-09-16 clasohm 1993-09-16 Initial revision