isabelle: File revisions

Mercurial Mercurial > repos > isabelle / file revisions

src/ZF/Datatype_ZF.thy

2015-09-09	wenzelm	simplified simproc programming interfaces;	file \| diff \| annotate
2015-07-23	wenzelm	isabelle update_cartouches;	file \| diff \| annotate
2015-02-10	wenzelm	proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;	file \| diff \| annotate
2014-11-02	wenzelm	modernized header;	file \| diff \| annotate
2014-10-30	wenzelm	eliminated aliases;	file \| diff \| annotate
2013-11-11	wenzelm	tuned signature -- removed obsolete Addsimprocs, Delsimprocs;	file \| diff \| annotate
2013-05-11	wenzelm	prefer explicitly qualified exceptions, which is particular important for robust handlers;	file \| diff \| annotate
2013-04-18	wenzelm	simplifier uses proper Proof.context instead of historic type simpset;	file \| diff \| annotate
2012-08-22	wenzelm	prefer ML_file over old uses;	file \| diff \| annotate
2012-03-15	wenzelm	declare command keywords via theory header, including strict checking outside Pure;	file \| diff \| annotate
2011-02-18	wenzelm	more precise headers;	file \| diff \| annotate
2010-08-25	wenzelm	renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;	file \| diff \| annotate
2010-08-18	haftmann	deglobalization	file \| diff \| annotate
2010-02-28	wenzelm	more antiquotations;	file \| diff \| annotate
2009-09-29	wenzelm	modernized Balanced_Tree;	file \| diff \| annotate
2009-09-29	wenzelm	explicit indication of Unsynchronized.ref;	file \| diff \| annotate
2009-08-28	wenzelm	modernized messages -- eliminated ctyp/cterm operations;	file \| diff \| annotate
2009-07-15	wenzelm	more antiquotations;	file \| diff \| annotate
2008-09-17	wenzelm	back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;	file \| diff \| annotate
2008-05-18	wenzelm	moved global pretty/string_of functions from Sign to Syntax;	file \| diff \| annotate
2008-05-17	wenzelm	structure Display: less pervasive operations;	file \| diff \| annotate
2008-03-29	wenzelm	replaced 'ML_setup' by 'ML';	file \| diff \| annotate
2008-02-11	krauss	Made theory names in ZF disjoint from HOL theory names to allow loading both developments	file \| diff \| annotate

less more (0) tip

isabelle

RSS Atom