| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
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;
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
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";
|
| #
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;
|
| #
3daff02d |
|
07-Oct-2007 |
wenzelm <none@none> |
replaced some 'translations' by 'abbreviation';
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
883f343f |
|
01-Feb-2005 |
paulson <none@none> |
the new subst tactic, by Lucas Dixon
|
| #
6f50ca35 |
|
23-Jan-2003 |
paulson <none@none> |
tidying (by script)
|
| #
4b2cdd98 |
|
27-Aug-2002 |
wenzelm <none@none> |
avoid duplicate fact bindings;
|
| #
d9f65115 |
|
14-Jul-2002 |
paulson <none@none> |
improved presentation markup
|
| #
1748209d |
|
03-Jul-2002 |
wenzelm <none@none> |
fixed comment;
|
| #
7aca62df |
|
02-Jul-2002 |
paulson <none@none> |
Tidying and introduction of various new theorems
|
| #
c1f9f84e |
|
28-Jun-2002 |
paulson <none@none> |
new theorems, tidying
|
| #
35633a0d |
|
18-Jun-2002 |
paulson <none@none> |
tidying
|
| #
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
|
| #
7eb302a3 |
|
23-May-2002 |
paulson <none@none> |
new definition of "apply" and new simprule "beta_if"
|
| #
91b19058 |
|
18-May-2002 |
paulson <none@none> |
converted Arith, Univ, func to Isar format!
|
| #
fea2e791 |
|
21-Jul-2000 |
paulson <none@none> |
Univ no longer requires Arith (really it never did)
|
| #
f3fcc93c |
|
12-Jan-1999 |
wenzelm <none@none> |
eliminated global/local names;
|
| #
b5894316 |
|
28-Dec-1998 |
paulson <none@none> |
new inductive, datatype and primrec packages, etc.
|
| #
0f61fff7 |
|
20-Oct-1997 |
wenzelm <none@none> |
local;
|
| #
12b5f959 |
|
17-Oct-1997 |
wenzelm <none@none> |
global;
|
| #
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
|
| #
8d325ec5 |
|
16-Dec-1994 |
lcp <none@none> |
now also depends upon Finite.thy
|
| #
38ec27bf |
|
28-Nov-1994 |
lcp <none@none> |
replaced "rules" by "defs"
|
| #
9df696ad |
|
11-Aug-1994 |
lcp <none@none> |
installation of new inductive/datatype sections
|
| #
3cf9f44b |
|
27-Jul-1994 |
lcp <none@none> |
Addition of infinite branching datatypes
|
| #
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
|
| #
7ee94368 |
|
08-Oct-1993 |
wenzelm <none@none> |
fixed comment;
|
| #
1d038aaa |
|
05-Oct-1993 |
lcp <none@none> |
Retry of the previous commit (network outage)
|
| #
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|