| #
001933f8 |
|
06-Mar-2012 |
paulson <none@none> |
mathematical symbols for Isabelle/ZF example theories
|
| #
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids;
tuned headers;
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
78231b68 |
|
10-Jul-2002 |
paulson <none@none> |
Fixed quantified variable name preservation for ball and bex (bounded quants)
Requires tweaking of other scripts. Also routine tidying.
|
| #
6c6c8702 |
|
25-Dec-2001 |
paulson <none@none> |
conversion to Isar
|
| #
09045852 |
|
21-May-2001 |
paulson <none@none> |
X-symbols for ZF
|
| #
f9168499 |
|
13-Jan-1999 |
paulson <none@none> |
datatype package improvements
|
| #
252953b8 |
|
07-Jan-1999 |
paulson <none@none> |
if-then-else syntax for ZF
|
| #
d5713f36 |
|
28-Dec-1998 |
paulson <none@none> |
converted to use new primrec section
|
| #
daf66f30 |
|
10-Oct-1997 |
wenzelm <none@none> |
fixed dots;
|
| #
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
|
| #
8ef6ec50 |
|
07-Mar-1995 |
lcp <none@none> |
Replaced rules by defs. Also got rid of tyconstU by
including TyConst in the datatype's universe
|
| #
ed2a2e5d |
|
28-Feb-1995 |
lcp <none@none> |
New example by Jacob Frost, tidied by lcp
|