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-07-01 |
paulson |
new lemmas, de-applying, etc.
|
file |
diff |
annotate
|
2018-06-06 |
paulson |
resolution of name clashes in Algebra
|
file |
diff |
annotate
|
2018-01-16 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
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-06 |
nipkow |
tuned op
|
file |
diff |
annotate
|
2017-12-02 |
haftmann |
more simplification rules
|
file |
diff |
annotate
|
2017-11-26 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2017-11-04 |
wenzelm |
prefer main entry points of HOL;
|
file |
diff |
annotate
|
2017-08-18 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
2017-04-06 |
haftmann |
session containing computational algebra
|
file |
diff |
annotate
|
2016-10-17 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
2016-10-17 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
2016-10-16 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
2016-08-08 |
eberlm |
is_prime -> prime
|
file |
diff |
annotate
|
2016-07-21 |
eberlm |
Overhaul of prime/multiplicity/prime_factors
|
file |
diff |
annotate
|
2016-05-26 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
2016-02-17 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
2015-12-28 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2015-11-04 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
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-07-05 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
2014-07-04 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
2014-03-07 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
2014-03-05 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2014-02-02 |
paulson |
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
|
file |
diff |
annotate
|
2014-01-27 |
paulson |
converting to new Number_Theory
|
file |
diff |
annotate
|
2012-10-19 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
2011-09-07 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
2011-09-02 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
2011-01-06 |
ballarin |
Abelian group facts obtained from group facts via interpretation (sublocale).
|
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-03-01 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
2009-11-13 |
nipkow |
moved lemma from Algebra/IntRing to Ring_and_Field
|
file |
diff |
annotate
|
2009-11-13 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
2009-09-01 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
|
2009-03-26 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
2009-02-17 |
nipkow |
Cleaned up IntDiv and removed subsumed lemmas.
|
file |
diff |
annotate
|
2009-01-31 |
nipkow |
added some simp rules
|
file |
diff |
annotate
|
2009-01-10 |
wenzelm |
fixed proof involving dvd;
|
file |
diff |
annotate
|
2008-12-19 |
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-10-07 |
haftmann |
arbitrary is undefined
|
file |
diff |
annotate
|
2008-09-02 |
ballarin |
Interpretation commands no longer accept interpretation attributes.
|
file |
diff |
annotate
|
2008-08-01 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
2008-07-30 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
file |
diff |
annotate
|
2008-01-15 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
2007-08-02 |
ballarin |
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
|
file |
diff |
annotate
|
2007-07-24 |
ballarin |
Interpretation of rings (as integers) maps defined operations to defined
|
file |
diff |
annotate
|
2007-01-12 |
ballarin |
Reverted to structure representation with records.
|
file |
diff |
annotate
|
2006-12-22 |
ballarin |
Experimenting with interpretations of "definition".
|
file |
diff |
annotate
|
2006-10-16 |
ballarin |
Order and lattice structures no longer based on records.
|
file |
diff |
annotate
|
2006-08-03 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
file |
diff |
annotate
|