| 2014-11-02 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| 2014-02-10 |
wenzelm |
prefer vacuous definitional type classes over axiomatic ones;
|
file |
diff |
annotate
|
| 2012-08-08 |
wenzelm |
proper axiomatization of "mem" -- do not leave it formally unspecified;
|
file |
diff |
annotate
|
| 2012-07-24 |
wenzelm |
clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
|
file |
diff |
annotate
|
| 2012-03-16 |
wenzelm |
modernized axiomatization;
|
file |
diff |
annotate
|
| 2012-03-13 |
paulson |
Structured proofs concerning the square of an infinite cardinal
|
file |
diff |
annotate
|
| 2012-03-06 |
paulson |
mathematical symbols instead of ASCII
|
file |
diff |
annotate
|
| 2012-03-01 |
paulson |
Removal of obsolete ML bindings
|
file |
diff |
annotate
|
| 2011-11-20 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| 2011-08-11 |
wenzelm |
redundant use of misc_legacy.ML;
|
file |
diff |
annotate
|
| 2011-02-18 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| 2010-12-20 |
wenzelm |
proper identifiers for consts and types;
|
file |
diff |
annotate
|
| 2010-12-17 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| 2010-11-26 |
wenzelm |
prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
|
file |
diff |
annotate
|
| 2010-09-03 |
wenzelm |
turned eta_contract into proper configuration option;
|
file |
diff |
annotate
|
| 2010-08-27 |
wenzelm |
expanded some aliases from structure Unsynchronized;
|
file |
diff |
annotate
|
| 2010-08-18 |
haftmann |
deglobalization
|
file |
diff |
annotate
|
| 2010-07-12 |
wenzelm |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
file |
diff |
annotate
|
| 2010-06-11 |
haftmann |
avoid references to old constdefs
|
file |
diff |
annotate
|
| 2010-02-11 |
wenzelm |
numeral syntax: clarify parse trees vs. actual terms;
|
file |
diff |
annotate
|
| 2010-02-09 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| 2009-10-17 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| 2009-09-29 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| 2008-07-29 |
ballarin |
Lemmas added
|
file |
diff |
annotate
|
| 2007-10-07 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| 2007-10-03 |
wenzelm |
avoid unnamed infixes;
|
file |
diff |
annotate
|
| 2007-05-31 |
wenzelm |
tuned ML setup;
|
file |
diff |
annotate
|
| 2006-01-29 |
wenzelm |
declare atomize/defn for Ball;
|
file |
diff |
annotate
|
| 2005-12-15 |
wenzelm |
removed obsolete/unused setup_induction;
|
file |
diff |
annotate
|
| 2005-10-07 |
wenzelm |
replaced _K by dummy abstraction;
|
file |
diff |
annotate
|
| 2005-06-17 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| 2005-02-01 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| 2004-06-08 |
paulson |
Groups, Rings and supporting lemmas
|
file |
diff |
annotate
|
| 2004-06-01 |
wenzelm |
removed obsolete sort 'logic';
|
file |
diff |
annotate
|
| 2004-04-14 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| 2003-10-10 |
paulson |
finalconsts
|
file |
diff |
annotate
|
| 2003-07-10 |
paulson |
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
|
file |
diff |
annotate
|
| 2003-06-27 |
paulson |
Conversion of AllocBase to new-style
|
file |
diff |
annotate
|
| 2003-01-15 |
paulson |
more new-style theories
|
file |
diff |
annotate
|
| 2002-05-23 |
paulson |
new definition of "apply" and new simprule "beta_if"
|
file |
diff |
annotate
|
| 2002-05-13 |
paulson |
quotes around types
|
file |
diff |
annotate
|
| 2002-05-08 |
paulson |
the new predicate "relation"
|
file |
diff |
annotate
|
| 2002-05-07 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2002-02-15 |
paulson |
a new definition of "restrict"
|
file |
diff |
annotate
|
| 2002-01-15 |
paulson |
split can now be unfolded even with one argument
|
file |
diff |
annotate
|
| 2001-12-19 |
paulson |
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
|
file |
diff |
annotate
|
| 2001-11-08 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| 2001-05-21 |
paulson |
fixed the X-symbol syntax for lambda
|
file |
diff |
annotate
|
| 2001-03-30 |
paulson |
the one-point rule for bounded quantifiers
|
file |
diff |
annotate
|
| 2000-09-14 |
wenzelm |
tuned spacing of symbols syntax;
|
file |
diff |
annotate
|
| 2000-08-24 |
paulson |
added some xsymbols, and tidied
|
file |
diff |
annotate
|
| 1999-03-10 |
wenzelm |
HTML output;
|
file |
diff |
annotate
|
| 1999-01-07 |
paulson |
if-then-else syntax for ZF
|
file |
diff |
annotate
|
| 1997-10-20 |
wenzelm |
local;
|
file |
diff |
annotate
|
| 1997-10-16 |
wenzelm |
global;
|
file |
diff |
annotate
|
| 1997-10-10 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| 1997-09-22 |
wenzelm |
tuned pattern syntax;
|
file |
diff |
annotate
|
| 1997-04-29 |
wenzelm |
deactivated new symbols (not yet printable on xterm, emacs);
|
file |
diff |
annotate
|
| 1997-04-29 |
wenzelm |
added \<langle>, \<rangle> symbols syntax;
|
file |
diff |
annotate
|
| 1997-04-02 |
paulson |
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
|
file |
diff |
annotate
|