isabelle: File revisions

src/FOLP/IFOLP.thy

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

isabelle

RSS Atom