| #
f8bf3c0e |
|
07-Nov-2019 |
wenzelm <none@none> |
tuned proofs -- more stable proof terms without [rule_format];
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
455aefc7 |
|
24-Jun-2018 |
wenzelm <none@none> |
simplified ZF theory names (in contrast to 6a0801279f4c): session-qualification already achieves disjointness;
--HG--
rename : src/ZF/Datatype_ZF.thy => src/ZF/Datatype.thy
rename : src/ZF/Inductive_ZF.thy => src/ZF/Inductive.thy
rename : src/ZF/Int_ZF.thy => src/ZF/Int.thy
rename : src/ZF/IntDiv_ZF.thy => src/ZF/IntDiv.thy
rename : src/ZF/List_ZF.thy => src/ZF/List.thy
rename : src/ZF/Nat_ZF.thy => src/ZF/Nat.thy
|
| #
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
|
| #
c8c5c95f |
|
19-Aug-2003 |
paulson <none@none> |
new case_tac
|
| #
db5797b1 |
|
30-May-2003 |
paulson <none@none> |
getting ZF/UNITY working again
|
| #
dd2a5068 |
|
27-May-2003 |
paulson <none@none> |
updating ZF-UNITY with Sidi's new material
|
| #
e43f07af |
|
19-Feb-2003 |
paulson <none@none> |
fixed anomalies in the installed classical rules
|
| #
6f50ca35 |
|
23-Jan-2003 |
paulson <none@none> |
tidying (by script)
|
| #
56765f7e |
|
04-Oct-2002 |
paulson <none@none> |
Various simplifications of the Constructible theories
|
| #
647bcb01 |
|
27-Aug-2002 |
wenzelm <none@none> |
*** empty log message ***
|
| #
43f1782a |
|
14-Jul-2002 |
paulson <none@none> |
Removal of mono.thy
|
| #
d9f65115 |
|
14-Jul-2002 |
paulson <none@none> |
improved presentation markup
|
| #
7aca62df |
|
02-Jul-2002 |
paulson <none@none> |
Tidying and introduction of various new theorems
|
| #
7d5ba449 |
|
05-Jun-2002 |
paulson <none@none> |
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
|
| #
b0abe6a7 |
|
28-May-2002 |
paulson <none@none> |
deleted some useless ML bindings
|
| #
0937f9be |
|
22-May-2002 |
paulson <none@none> |
more tidying
|
| #
fdb391ee |
|
22-May-2002 |
paulson <none@none> |
new version of nat_case, nat_case3
|
| #
c0ab4494 |
|
22-May-2002 |
paulson <none@none> |
conversion of Nat to Isar
|
| #
d49e01e7 |
|
16-Jan-2002 |
paulson <none@none> |
new definitions from Sidi Ehmety
|
| #
f3f91f1c |
|
03-Jan-1997 |
paulson <none@none> |
Implicit simpsets and clasets for FOL and ZF
|
| #
49ebaab4 |
|
05-Feb-1996 |
clasohm <none@none> |
expanded tabs
|
| #
cc52541b |
|
09-Dec-1995 |
clasohm <none@none> |
removed quotes from consts and syntax sections
|
| #
da37c2f7 |
|
22-Jun-1995 |
clasohm <none@none> |
removed \...\ inside strings
|
| #
38ec27bf |
|
28-Nov-1994 |
lcp <none@none> |
replaced "rules" by "defs"
|
| #
ba6b9f3c |
|
21-Jun-1994 |
lcp <none@none> |
Addition of cardinals and order types, various tidying
|
| #
5c777ea1 |
|
16-Nov-1993 |
clasohm <none@none> |
made pseudo theories for all ML files;
documented dependencies between all thy and ML files
|
| #
ce0256d3 |
|
17-Sep-1993 |
lcp <none@none> |
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
|
| #
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|