#
9fd71573 |
|
10-Jun-2014 |
Thomas Sewell <thomas.sewell@nicta.com.au> |
Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change. --HG-- extra : rebase_source : b0150e06a14c2821e03208834282be6eca87aae0
|
#
001933f8 |
|
06-Mar-2012 |
paulson <none@none> |
mathematical symbols for Isabelle/ZF example theories
|
#
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;
|
#
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.
|
#
6ab7a33a |
|
29-Dec-2001 |
wenzelm <none@none> |
tuned document sources;
|
#
6c6c8702 |
|
25-Dec-2001 |
paulson <none@none> |
conversion to Isar
|
#
09045852 |
|
21-May-2001 |
paulson <none@none> |
X-symbols for ZF
|
#
9609c2b0 |
|
13-Jan-1999 |
paulson <none@none> |
tidying of datatype and inductive definitions
|
#
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
|
#
be808235 |
|
07-Mar-1995 |
lcp <none@none> |
Replaced rules by defs
|
#
8df51977 |
|
27-Feb-1995 |
lcp <none@none> |
New example by Jacob Frost, tidied by lcp
|