src/FOLP/IFOLP.thy
2010-12-20 wenzelm proper identifiers for consts and types;
2010-09-20 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-27 wenzelm proper configuration option "show_proofs";
2010-08-18 haftmann deglobalization
2010-04-28 wenzelm renamed command 'defaultsort' to 'default_sort';
2010-04-23 wenzelm mark schematic statements explicitly;
2010-02-15 wenzelm eliminated unnamed infixes;
2010-02-11 wenzelm modernized translations;
2009-09-29 wenzelm explicit indication of Unsynchronized.ref;
2009-01-02 wenzelm fixed assumption proof;
2008-12-31 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-06-11 wenzelm changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;
2008-06-11 wenzelm tuned comments;
2008-05-18 wenzelm setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
2008-03-29 wenzelm replaced 'ML_setup' by 'ML';
2008-03-18 wenzelm converted legacy ML scripts;
2005-09-18 wenzelm converted to Isar theory format;
2004-06-01 wenzelm removed obsolete sort 'logic';
1999-04-26 paulson fixed a bug many years old in rule plusEC
1997-10-20 wenzelm adapted to qualified names;
1997-10-10 wenzelm fixed dots;
1997-03-04 paulson Removed needless quotes
1996-02-05 clasohm expanded tabs
1995-06-21 clasohm removed \...\ inside strings
1995-06-02 lcp Corrected comments in headers
1994-10-21 lcp FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
1994-03-17 lcp new type declaration syntax instead of numbers
1993-09-16 clasohm Initial revision
less more (0) tip