| #
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;
|
| #
e2e4d5f1 |
|
03-Jan-2019 |
wenzelm <none@none> |
isabelle update -u mixfix_cartouches;
|
| #
ad00661e |
|
16-Sep-2016 |
wenzelm <none@none> |
more symbols;
|
| #
8ecffcf0 |
|
23-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
2257dcda |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
0551f7de |
|
01-Nov-2014 |
wenzelm <none@none> |
eliminated spurious semicolons;
|
| #
ed870e69 |
|
15-Mar-2012 |
paulson <none@none> |
replacing ":" by "\<in>"
|
| #
8125fbfb |
|
06-Mar-2012 |
paulson <none@none> |
Using mathematical notation for <-> and cardinal arithmetic
|
| #
f902d62a |
|
06-Mar-2012 |
paulson <none@none> |
mathematical symbols instead of ASCII
|
| #
adfe6cf9 |
|
17-Dec-2010 |
wenzelm <none@none> |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
4566f6ab |
|
29-Jul-2008 |
ballarin <none@none> |
Lemmas added
|
| #
84502ed9 |
|
11-Jun-2008 |
wenzelm <none@none> |
tuned comments;
|
| #
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
|
| #
886424e5 |
|
08-Jun-2004 |
paulson <none@none> |
Groups, Rings and supporting lemmas
|
| #
c8c5c95f |
|
19-Aug-2003 |
paulson <none@none> |
new case_tac
|
| #
f5ea3b4a |
|
10-Jul-2003 |
paulson <none@none> |
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
variable
|
| #
dd2a5068 |
|
27-May-2003 |
paulson <none@none> |
updating ZF-UNITY with Sidi's new material
|
| #
32a75c4c |
|
01-Oct-2002 |
paulson <none@none> |
Numerous cosmetic changes, prompted by the new simplifier
|
| #
43f1782a |
|
14-Jul-2002 |
paulson <none@none> |
Removal of mono.thy
|
| #
c539a306 |
|
14-Jul-2002 |
paulson <none@none> |
merged Update with func
|
| #
7aca62df |
|
02-Jul-2002 |
paulson <none@none> |
Tidying and introduction of various new theorems
|
| #
9ff82ede |
|
26-Jun-2002 |
paulson <none@none> |
new theorems
|
| #
4070dfc0 |
|
19-Jun-2002 |
paulson <none@none> |
conversion of Cardinal, CardinalArith
|
| #
8e86958c |
|
18-Jun-2002 |
paulson <none@none> |
new lemma
|
| #
fae00c42 |
|
24-May-2002 |
paulson <none@none> |
strong lemmas about functions
|
| #
f4cdbecf |
|
24-May-2002 |
paulson <none@none> |
conversion of Perm to Isar. Strengthening of comp_fun_apply
|
| #
7eb302a3 |
|
23-May-2002 |
paulson <none@none> |
new definition of "apply" and new simprule "beta_if"
|
| #
0937f9be |
|
22-May-2002 |
paulson <none@none> |
more tidying
|
| #
ffcfb391 |
|
22-May-2002 |
paulson <none@none> |
tidying up
|
| #
f4e55b29 |
|
21-May-2002 |
paulson <none@none> |
converted domrange to Isar and merged with equalities
|
| #
91b19058 |
|
18-May-2002 |
paulson <none@none> |
converted Arith, Univ, func to Isar format!
|
| #
f3f91f1c |
|
03-Jan-1997 |
paulson <none@none> |
Implicit simpsets and clasets for FOL and ZF
|
| #
f14f9e3d |
|
15-Aug-1994 |
lcp <none@none> |
ZF/func/empty_fun: renamed from fun_empty
ZF/func/single_fun: replaces the weaker fun_single
ZF/func/fun_single_lemma: deleted
ZF/func.thy: now depends upon equalities.thy
|
| #
5c777ea1 |
|
16-Nov-1993 |
clasohm <none@none> |
made pseudo theories for all ML files;
documented dependencies between all thy and ML files
|