| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
e2e4d5f1 |
|
03-Jan-2019 |
wenzelm <none@none> |
isabelle update -u mixfix_cartouches;
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
2531ee45 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
a0a64492 |
|
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;
|
| #
e1f0bba9 |
|
11-Sep-2014 |
blanchet <none@none> |
fixed some spelling mistakes
|
| #
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
|
| #
ed870e69 |
|
15-Mar-2012 |
paulson <none@none> |
replacing ":" by "\<in>"
|
| #
001933f8 |
|
06-Mar-2012 |
paulson <none@none> |
mathematical symbols for Isabelle/ZF example theories
|
| #
29168e90 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
7882ab22 |
|
11-Feb-2010 |
wenzelm <none@none> |
numeral syntax: clarify parse trees vs. actual terms;
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
a58d8e0d |
|
26-Mar-2008 |
wenzelm <none@none> |
rule swap: renamed Pa to P;
|
| #
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';
|
| #
8a8582cc |
|
08-Oct-2006 |
wenzelm <none@none> |
attribute symmetric: zero_var_indexes;
|
| #
8922a0f2 |
|
15-Dec-2005 |
wenzelm <none@none> |
improved proofs;
|
| #
678cd7d2 |
|
01-Aug-2005 |
wenzelm <none@none> |
simprocs: Simplifier.inherit_bounds;
|
| #
883f343f |
|
01-Feb-2005 |
paulson <none@none> |
the new subst tactic, by Lucas Dixon
|
| #
2857bf15 |
|
17-Sep-2004 |
paulson <none@none> |
converted ZF/Induct/Multiset to Isar script
|
| #
dd2a5068 |
|
27-May-2003 |
paulson <none@none> |
updating ZF-UNITY with Sidi's new material
|
| #
73159505 |
|
14-Feb-2002 |
paulson <none@none> |
a new definition of "restrict"
|
| #
0ff58169 |
|
29-Jan-2002 |
paulson <none@none> |
Multiset: added the translation Mult(A) => A-||>nat-{0}
(which internalises the `multiset' relation).
FoldSet: weakened the typing conditions of the function f and
(by the way) removed the `locale' declarations.
|
| #
6ab7a33a |
|
29-Dec-2001 |
wenzelm <none@none> |
tuned document sources;
|
| #
f532bfa1 |
|
07-Nov-2001 |
paulson <none@none> |
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
Also, fixes to the cancellation simprocs and a few new standard lemmas.
|