src/FOLP/IFOLP.thy
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