| #
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;
|
| #
eea43a21 |
|
30-Dec-2015 |
wenzelm <none@none> |
clarified syntax;
|
| #
2531ee45 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
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;
|
| #
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
|
| #
29168e90 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;
|
| #
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids;
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
|
| #
886424e5 |
|
08-Jun-2004 |
paulson <none@none> |
Groups, Rings and supporting lemmas
|
| #
7654e199 |
|
27-Aug-2003 |
skalberg <none@none> |
Extended the notion of letter and digit, such that now one may use greek,
gothic, euler, or calligraphic letters as normal letters.
|
| #
f5ea3b4a |
|
10-Jul-2003 |
paulson <none@none> |
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
variable
|
| #
ba600295 |
|
30-Jun-2003 |
paulson <none@none> |
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
Conversion of UNITY/State to Isar format.;
|
| #
d108d75e |
|
27-Jun-2003 |
paulson <none@none> |
Conversion of theory UNITY to Isar script
|
| #
65e75de5 |
|
27-Jun-2003 |
paulson <none@none> |
Conversion of AllocBase to new-style
|
| #
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
|
| #
882c4d7c |
|
23-Apr-2003 |
paulson <none@none> |
Got rid of the [iff], which was effectively inserting converseD
|
| #
32a75c4c |
|
01-Oct-2002 |
paulson <none@none> |
Numerous cosmetic changes, prompted by the new simplifier
|
| #
ceac7595 |
|
30-Sep-2002 |
berghofe <none@none> |
Adapted to new simplifier.
|
| #
287028e5 |
|
28-Aug-2002 |
paulson <none@none> |
various new lemmas for Constructible
|
| #
43f1782a |
|
14-Jul-2002 |
paulson <none@none> |
Removal of mono.thy
|
| #
d9f65115 |
|
14-Jul-2002 |
paulson <none@none> |
improved presentation markup
|
| #
fe0050dc |
|
29-Jun-2002 |
paulson <none@none> |
conversion of many files to Isar format
|
| #
9ff82ede |
|
26-Jun-2002 |
paulson <none@none> |
new theorems
|
| #
7d5ba449 |
|
05-Jun-2002 |
paulson <none@none> |
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
|
| #
d0f34473 |
|
24-May-2002 |
paulson <none@none> |
new quantifier lemmas
|
| #
0937f9be |
|
22-May-2002 |
paulson <none@none> |
more tidying
|
| #
ffcfb391 |
|
22-May-2002 |
paulson <none@none> |
tidying up
|
| #
d461a545 |
|
21-May-2002 |
paulson <none@none> |
conversion of OrdQuant.ML to Isar
|
| #
f4e55b29 |
|
21-May-2002 |
paulson <none@none> |
converted domrange to Isar and merged with equalities
|
| #
2a14c840 |
|
20-May-2002 |
paulson <none@none> |
conversion of equalities and WF to Isar
|
| #
f3f91f1c |
|
03-Jan-1997 |
paulson <none@none> |
Implicit simpsets and clasets for FOL and ZF
|
| #
50498322 |
|
15-Aug-1994 |
lcp <none@none> |
ZF/equalities/Sigma_cons: new
ZF/equalities/cons_eq: new
ZF/equalities.thy: added final newline
|
| #
5c777ea1 |
|
16-Nov-1993 |
clasohm <none@none> |
made pseudo theories for all ML files;
documented dependencies between all thy and ML files
|