| 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
|
| 1997-01-23 |
wenzelm |
added symbols syntax;
|
file |
diff |
annotate
|
| 1997-01-03 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| 1996-12-02 |
wenzelm |
removed out-dated comment;
|
file |
diff |
annotate
|
| 1996-02-06 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| 1995-12-09 |
clasohm |
removed quotes from consts and syntax sections
|
file |
diff |
annotate
|
| 1995-06-22 |
clasohm |
removed \...\ inside strings
|
file |
diff |
annotate
|
| 1995-05-10 |
nipkow |
Modified translation for pattern abstraction.
|
file |
diff |
annotate
|
| 1995-05-04 |
lcp |
Added pattern-matching code from CHOL/Prod.thy. Changed
|
file |
diff |
annotate
|
| 1994-11-03 |
lcp |
ZF: NEW DEFINITION OF PI(A,B)
|
file |
diff |
annotate
|
| 1994-10-31 |
lcp |
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
|
file |
diff |
annotate
|
| 1994-10-12 |
wenzelm |
fixed infix names in print_translations;
|
file |
diff |
annotate
|
| 1994-09-21 |
wenzelm |
minor cleanup, added 'syntax' section;
|
file |
diff |
annotate
|
| 1994-08-12 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|
| 1994-07-26 |
lcp |
Axiom of choice, cardinality results, etc.
|
file |
diff |
annotate
|
| 1994-05-03 |
lcp |
removal of obsolete type-declaration syntax
|
file |
diff |
annotate
|
| 1993-10-25 |
wenzelm |
added white-space;
|
file |
diff |
annotate
|
| 1993-10-11 |
wenzelm |
"The" now a binder, removed translation;
|
file |
diff |
annotate
|
| 1993-10-07 |
lcp |
added ~: for "not in"
|
file |
diff |
annotate
|
| 1993-09-16 |
clasohm |
Initial revision
|
file |
diff |
annotate
|