| #
e2e4d5f1 |
|
03-Jan-2019 |
wenzelm <none@none> |
isabelle update -u mixfix_cartouches;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
ad00661e |
|
16-Sep-2016 |
wenzelm <none@none> |
more symbols;
|
| #
2531ee45 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
fb38f9dd |
|
10-Oct-2015 |
wenzelm <none@none> |
tuned syntax -- more symbols;
|
| #
8ecffcf0 |
|
23-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
68f43bed |
|
23-Mar-2015 |
wenzelm <none@none> |
prefer local fixes;
|
| #
2257dcda |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
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
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
f08efa79 |
|
29-Jul-2008 |
ballarin <none@none> |
Definitions and some lemmas for reflexive orderings.
|
| #
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
|
| #
d172768b |
|
08-Nov-2002 |
paulson <none@none> |
generalized wf_on_unit to wf_on_any_0
|
| #
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.
|
| #
d9f65115 |
|
14-Jul-2002 |
paulson <none@none> |
improved presentation markup
|
| #
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.
|
| #
22ae70e0 |
|
14-Jun-2002 |
paulson <none@none> |
better proof of ord_iso_restrict_pred
|
| #
b0abe6a7 |
|
28-May-2002 |
paulson <none@none> |
deleted some useless ML bindings
|
| #
f4cdbecf |
|
24-May-2002 |
paulson <none@none> |
conversion of Perm to Isar. Strengthening of comp_fun_apply
|
| #
4607f228 |
|
13-May-2002 |
paulson <none@none> |
converted Order.ML OrderType.ML OrderArith.ML to Isar format
|
| #
70d24ce0 |
|
08-May-2002 |
paulson <none@none> |
better xsymbol syntax
|
| #
657cb345 |
|
24-Aug-2000 |
paulson <none@none> |
added some xsymbols, and tidied
|
| #
f3f91f1c |
|
03-Jan-1997 |
paulson <none@none> |
Implicit simpsets and clasets for FOL and ZF
|
| #
41e8a3bd |
|
11-Jul-1996 |
paulson <none@none> |
Corrected indentation
|
| #
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
|
| #
bd44cfd4 |
|
14-Dec-1994 |
lcp <none@none> |
added constants mono_map, ord_iso_map
|
| #
37eef679 |
|
24-Aug-1994 |
lcp <none@none> |
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
the keyword "inductive" making the theory file fail
ZF/Makefile: now has Inductive.thy,.ML
ZF/Datatype,Finite,Zorn: depend upon Inductive
ZF/intr_elim: now checks that the inductive name does not clash with
existing theory names
ZF/ind_section: deleted things replicated in Pure/section_utils.ML
ZF/ROOT: now loads Pure/section_utils
|
| #
ba6b9f3c |
|
21-Jun-1994 |
lcp <none@none> |
Addition of cardinals and order types, various tidying
|