| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
e2e4d5f1 |
|
03-Jan-2019 |
wenzelm <none@none> |
isabelle update -u mixfix_cartouches;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
74c9a8d5 |
|
09-Apr-2017 |
wenzelm <none@none> |
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
--HG--
rename : src/ZF/Main_ZF.thy => src/ZF/ZF.thy
rename : src/ZF/Main_ZFC.thy => src/ZF/ZFC.thy
rename : src/ZF/ZF.thy => src/ZF/ZF_Base.thy
|
| #
56a6bda0 |
|
10-Oct-2015 |
wenzelm <none@none> |
tuned syntax -- more symbols;
|
| #
8ecffcf0 |
|
23-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
001933f8 |
|
06-Mar-2012 |
paulson <none@none> |
mathematical symbols for Isabelle/ZF example theories
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
e7a16ceb |
|
07-Oct-2007 |
wenzelm <none@none> |
modernized specifications;
removed legacy ML bindings;
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
6f40aa86 |
|
24-Jun-2003 |
paulson <none@none> |
Converting ZF/UNITY to Isar
|
| #
dd2a5068 |
|
27-May-2003 |
paulson <none@none> |
updating ZF-UNITY with Sidi's new material
|
| #
0c82a740 |
|
31-May-2002 |
paulson <none@none> |
conversion of Finite to Isar format
|
| #
0ff58169 |
|
29-Jan-2002 |
paulson <none@none> |
Multiset: added the translation Mult(A) => A-||>nat-{0}
(which internalises the `multiset' relation).
FoldSet: weakened the typing conditions of the function f and
(by the way) removed the `locale' declarations.
|
| #
6ab7a33a |
|
29-Dec-2001 |
wenzelm <none@none> |
tuned document sources;
|
| #
f532bfa1 |
|
07-Nov-2001 |
paulson <none@none> |
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
Also, fixes to the cancellation simprocs and a few new standard lemmas.
|