2019-01-05 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
2018-09-24 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
2018-06-14 |
paulson |
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
|
file |
diff |
annotate
|
2018-02-15 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2018-01-10 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
2018-01-10 |
nipkow |
tuned op's
|
file |
diff |
annotate
|
2018-01-05 |
nipkow |
Renamed (^) to [^] in preparation of the move from "op X" to (X)
|
file |
diff |
annotate
|
2017-11-26 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2017-01-17 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2016-09-16 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2016-05-26 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
2015-11-04 |
ballarin |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
file |
diff |
annotate
|
2015-10-27 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
2015-10-10 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
2015-10-10 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
2015-09-13 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
2015-04-17 |
Rene Thiemann |
finprod takes 1 in case of infinite sets => remove several "finite A" assumptions
|
file |
diff |
annotate
|
2014-10-07 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
2014-08-05 |
wenzelm |
tuned proofs -- fewer warnings;
|
file |
diff |
annotate
|
2014-07-04 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
2014-03-05 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2013-12-25 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
2012-10-19 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
2011-09-12 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
2011-09-07 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
2011-09-02 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
2010-08-02 |
ballarin |
Revised proof of long division contributed by Jesus Aransay.
|
file |
diff |
annotate
|
2010-04-07 |
ballarin |
Merged resolving conflicts NEWS and locale.ML.
|
file |
diff |
annotate
|
2010-02-15 |
ballarin |
Tuned interpretation proofs.
|
file |
diff |
annotate
|
2010-03-21 |
wenzelm |
standard headers;
|
file |
diff |
annotate
|
2010-03-21 |
wenzelm |
slightly more uniform definitions -- eliminated old-style meta-equality;
|
file |
diff |
annotate
|
2010-01-10 |
berghofe |
Adapted to changes in induct method.
|
file |
diff |
annotate
|
2009-11-13 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
2009-10-17 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
2009-08-31 |
nipkow |
tuned the simp rules for Int involving insert and intervals.
|
file |
diff |
annotate
|
2009-08-28 |
nipkow |
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
|
file |
diff |
annotate
|
2009-03-26 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
2009-03-08 |
wenzelm |
proper local context for text with antiquotations;
|
file |
diff |
annotate
|
2008-12-19 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
2008-12-17 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
2008-12-16 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
2008-11-17 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
2008-08-18 |
ballarin |
Theorem on polynomial division and lemmas.
|
file |
diff |
annotate
|
2008-08-01 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
2008-07-31 |
ballarin |
Tuned (for the sake of a meaningless log entry).
|
file |
diff |
annotate
|
2008-07-15 |
ballarin |
Removed uses of context element includes.
|
file |
diff |
annotate
|
2008-05-17 |
wenzelm |
avoid undeclared variables within proofs;
|
file |
diff |
annotate
|
2008-03-05 |
wenzelm |
explicit referencing of background facts;
|
file |
diff |
annotate
|
2007-06-12 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
2007-05-10 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
2006-11-23 |
wenzelm |
prefer antiquotations over LaTeX macros;
|
file |
diff |
annotate
|
2006-08-30 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
2006-08-03 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
file |
diff |
annotate
|
2006-08-02 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
2006-07-26 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
2006-07-04 |
ballarin |
Method intro_locales replaced by intro_locales and unfold_locales.
|
file |
diff |
annotate
|
2006-06-20 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
2006-06-06 |
ballarin |
Improved parameter management of locales.
|
file |
diff |
annotate
|
2006-05-05 |
wenzelm |
get rid of 'concl is';
|
file |
diff |
annotate
|
2005-08-17 |
ballarin |
Use interpretation in locales.
|
file |
diff |
annotate
|
2005-07-01 |
berghofe |
Removed setsubgoaler hack (thanks to strengthened finsum_cong).
|
file |
diff |
annotate
|
2005-06-17 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
2005-05-09 |
paulson |
from simplesubst to new subst
|
file |
diff |
annotate
|
2005-04-18 |
ballarin |
Interpretation supports statically scoped attributes; documentation.
|
file |
diff |
annotate
|
2005-04-11 |
ballarin |
First release of interpretation commands.
|
file |
diff |
annotate
|
2005-03-09 |
ballarin |
First version of global registration command.
|
file |
diff |
annotate
|
2005-02-01 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
2004-08-02 |
ballarin |
Theories now take advantage of recent syntax improvements with (structure).
|
file |
diff |
annotate
|
2004-07-26 |
ballarin |
New prover for transitive and reflexive-transitive closure of relations.
|
file |
diff |
annotate
|
2004-07-15 |
nipkow |
Moved to new m<..<n syntax for set intervals.
|
file |
diff |
annotate
|
2004-06-17 |
paulson |
removal of magmas and semigroups
|
file |
diff |
annotate
|
2004-05-06 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
2004-04-23 |
wenzelm |
improved notation;
|
file |
diff |
annotate
|
2004-04-22 |
wenzelm |
improved notation;
|
file |
diff |
annotate
|
2004-04-16 |
wenzelm |
simplified ML code for setsubgoaler;
|
file |
diff |
annotate
|
2004-04-16 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
2004-04-13 |
ballarin |
Added brief intro text.
|
file |
diff |
annotate
|
2004-02-19 |
ballarin |
New lemmas about inversion of restricted functions.
|
file |
diff |
annotate
|
2003-05-07 |
ballarin |
Small changes for release Isabelle 2003.
|
file |
diff |
annotate
|
2003-05-02 |
ballarin |
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
|
file |
diff |
annotate
|
2003-04-30 |
ballarin |
HOL-Algebra: New polynomial development added.
|
file |
diff |
annotate
|