| 2007-05-31 |
wenzelm |
2007-05-31 |
tuned ML setup;
|
file | diff | annotate |
| 2006-01-29 |
wenzelm |
2006-01-29 |
declare atomize/defn for Ball;
|
file | diff | annotate |
| 2005-12-15 |
wenzelm |
2005-12-15 |
removed obsolete/unused setup_induction;
|
file | diff | annotate |
| 2005-10-07 |
wenzelm |
2005-10-07 |
replaced _K by dummy abstraction;
|
file | diff | annotate |
| 2005-06-17 |
haftmann |
2005-06-17 |
migrated theory headers to new format
|
file | diff | annotate |
| 2005-02-01 |
paulson |
2005-02-01 |
the new subst tactic, by Lucas Dixon
|
file | diff | annotate |
| 2004-06-08 |
paulson |
2004-06-08 |
Groups, Rings and supporting lemmas
|
file | diff | annotate |
| 2004-06-01 |
wenzelm |
2004-06-01 |
removed obsolete sort 'logic';
|
file | diff | annotate |
| 2004-04-14 |
kleing |
2004-04-14 |
use more symbols in HTML output
|
file | diff | annotate |
| 2003-10-10 |
paulson |
2003-10-10 |
finalconsts
|
file | diff | annotate |
| 2003-07-10 |
paulson |
2003-07-10 |
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
variable
|
file | diff | annotate |
| 2003-06-27 |
paulson |
2003-06-27 |
Conversion of AllocBase to new-style
|
file | diff | annotate |
| 2003-01-15 |
paulson |
2003-01-15 |
more new-style theories
|
file | diff | annotate |
| 2002-05-23 |
paulson |
2002-05-23 |
new definition of "apply" and new simprule "beta_if"
|
file | diff | annotate |
| 2002-05-13 |
paulson |
2002-05-13 |
quotes around types
|
file | diff | annotate |
| 2002-05-08 |
paulson |
2002-05-08 |
the new predicate "relation"
|
file | diff | annotate |
| 2002-05-07 |
wenzelm |
2002-05-07 |
tuned;
|
file | diff | annotate |
| 2002-02-15 |
paulson |
2002-02-15 |
a new definition of "restrict"
|
file | diff | annotate |
| 2002-01-15 |
paulson |
2002-01-15 |
split can now be unfolded even with one argument
|
file | diff | annotate |
| 2001-12-19 |
paulson |
2001-12-19 |
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
|
file | diff | annotate |
| 2001-11-09 |
wenzelm |
2001-11-09 |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file | diff | annotate |
| 2001-05-21 |
paulson |
2001-05-21 |
fixed the X-symbol syntax for lambda
|
file | diff | annotate |
| 2001-03-30 |
paulson |
2001-03-30 |
the one-point rule for bounded quantifiers
|
file | diff | annotate |
| 2000-09-15 |
wenzelm |
2000-09-15 |
tuned spacing of symbols syntax;
enabled langle and rangle in xsymbols syntax;
|
file | diff | annotate |
| 2000-08-24 |
paulson |
2000-08-24 |
added some xsymbols, and tidied
|
file | diff | annotate |
| 1999-03-10 |
wenzelm |
1999-03-10 |
HTML output;
|
file | diff | annotate |
| 1999-01-07 |
paulson |
1999-01-07 |
if-then-else syntax for ZF
|
file | diff | annotate |
| 1997-10-20 |
wenzelm |
1997-10-20 |
local;
|
file | diff | annotate |
| 1997-10-16 |
wenzelm |
1997-10-16 |
global;
|
file | diff | annotate |
| 1997-10-10 |
wenzelm |
1997-10-10 |
fixed dots;
|
file | diff | annotate |
| 1997-09-22 |
wenzelm |
1997-09-22 |
tuned pattern syntax;
|
file | diff | annotate |
| 1997-04-29 |
wenzelm |
1997-04-29 |
deactivated new symbols (not yet printable on xterm, emacs);
|
file | diff | annotate |
| 1997-04-29 |
wenzelm |
1997-04-29 |
added \<langle>, \<rangle> symbols syntax;
|
file | diff | annotate |
| 1997-04-02 |
paulson |
1997-04-02 |
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
|
file | diff | annotate |
| 1997-01-23 |
wenzelm |
1997-01-23 |
added symbols syntax;
|
file | diff | annotate |
| 1997-01-03 |
paulson |
1997-01-03 |
Implicit simpsets and clasets for FOL and ZF
|
file | diff | annotate |
| 1996-12-02 |
wenzelm |
1996-12-02 |
removed out-dated comment;
|
file | diff | annotate |
| 1996-02-06 |
clasohm |
1996-02-06 |
expanded tabs
|
file | diff | annotate |
| 1995-12-09 |
clasohm |
1995-12-09 |
removed quotes from consts and syntax sections
|
file | diff | annotate |
| 1995-06-22 |
clasohm |
1995-06-22 |
removed \...\ inside strings
|
file | diff | annotate |
| 1995-05-10 |
nipkow |
1995-05-10 |
Modified translation for pattern abstraction.
|
file | diff | annotate |
| 1995-05-04 |
lcp |
1995-05-04 |
Added pattern-matching code from CHOL/Prod.thy. Changed
definitions so that split is now defined in terms of fst, snd. Now split is
polymorphic. Deleted fsplit, as split(...)::o gives a similar effect -- NOT
identical though, as fsplit(P,z) implied that z was a pair, while split(P,z)
means only P(fst(z),snd(z)).
|
file | diff | annotate |
| 1994-11-03 |
lcp |
1994-11-03 |
ZF: NEW DEFINITION OF PI(A,B)
Was Pi(A,B) == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f}
Now function(r) == ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y')
Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
This simplifies many proofs, since (a) the top-level definition has fewer
bound variables (b) the "total" and "function" properties are separated
(c) the awkward EX! quantifier is eliminated.
ZF/ZF.thy/function: new definition
|
file | diff | annotate |
| 1994-10-31 |
lcp |
1994-10-31 |
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
|
file | diff | annotate |
| 1994-10-12 |
wenzelm |
1994-10-12 |
fixed infix names in print_translations;
|
file | diff | annotate |
| 1994-09-21 |
wenzelm |
1994-09-21 |
minor cleanup, added 'syntax' section;
|
file | diff | annotate |
| 1994-08-12 |
lcp |
1994-08-12 |
installation of new inductive/datatype sections
|
file | diff | annotate |
| 1994-07-26 |
lcp |
1994-07-26 |
Axiom of choice, cardinality results, etc.
|
file | diff | annotate |
| 1994-05-03 |
lcp |
1994-05-03 |
removal of obsolete type-declaration syntax
|
file | diff | annotate |
| 1993-10-25 |
wenzelm |
1993-10-25 |
added white-space;
made ~: a fake infix;
|
file | diff | annotate |
| 1993-10-11 |
wenzelm |
1993-10-11 |
"The" now a binder, removed translation;
improved encoding and translations of tuples;
added parse rules for -> and *, removed ndependent_tr;
|
file | diff | annotate |
| 1993-10-07 |
lcp |
1993-10-07 |
added ~: for "not in"
|
file | diff | annotate |
| 1993-09-16 |
clasohm |
1993-09-16 |
Initial revision
|
file | diff | annotate |