| 2017-11-26 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2016-12-17 |
haftmann |
reoriented congruence rules in non-explosive direction
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
dropped potentially explosive rule for groebner simpset, with no observable effect on examples
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
simplified fact references
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| 2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2015-10-18 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2014-11-07 |
wenzelm |
more accurate keywords;
|
file |
diff |
annotate
|
| 2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| 2014-10-23 |
haftmann |
further downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| 2014-08-16 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| 2014-05-04 |
blanchet |
added 'satx' proof method to Try0
|
file |
diff |
annotate
|
| 2014-02-16 |
haftmann |
eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)
|
file |
diff |
annotate
|
| 2014-01-30 |
blanchet |
added 'algebra' and 'meson' to 'try0'
|
file |
diff |
annotate
|
| 2013-11-04 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| 2012-08-22 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| 2012-04-12 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
remove duplicate [algebra] declarations
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
generalize more div/mod lemmas
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
generalize some theorems about div/mod
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| 2011-10-28 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
| 2010-05-07 |
haftmann |
delete Groebner_Basis directory -- only one file left
|
file |
diff |
annotate
|
| 2010-05-07 |
haftmann |
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
|
file |
diff |
annotate
|
| 2010-05-06 |
haftmann |
proper sublocales; no free-floating ML sections
|
file |
diff |
annotate
|
| 2010-05-06 |
haftmann |
moved generic lemmas to appropriate places
|
file |
diff |
annotate
|
| 2010-05-06 |
haftmann |
dropped duplicate comp_arith
|
file |
diff |
annotate
|
| 2010-05-06 |
haftmann |
avoid references to groebner bases in names which have no references to groebner bases
|
file |
diff |
annotate
|
| 2010-05-06 |
haftmann |
moved presimplification rules for algebraic methods into named thms functor
|
file |
diff |
annotate
|
| 2010-05-06 |
haftmann |
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
|
file |
diff |
annotate
|
| 2010-05-05 |
haftmann |
moved nat_arith ot Nat_Numeral: clarified normalizer setup
|
file |
diff |
annotate
|
| 2010-05-05 |
haftmann |
dropped unused file
|
file |
diff |
annotate
|
| 2010-04-26 |
haftmann |
use new classes (linordered_)field_inverse_zero
|
file |
diff |
annotate
|
| 2010-04-26 |
haftmann |
class division_ring_inverse_zero
|
file |
diff |
annotate
|
| 2010-04-23 |
haftmann |
dequalified fact name
|
file |
diff |
annotate
|
| 2010-02-28 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| 2010-02-18 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| 2010-02-10 |
haftmann |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
file |
diff |
annotate
|
| 2010-02-10 |
haftmann |
moved constants inverse and divide to Ring.thy
|
file |
diff |
annotate
|
| 2010-02-08 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| 2010-01-28 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| 2009-10-30 |
haftmann |
combined former theories Divides and IntDiv to one theory Divides
|
file |
diff |
annotate
|
| 2009-10-28 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
| 2009-06-24 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
| 2009-05-08 |
haftmann |
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
|
file |
diff |
annotate
|
| 2009-04-28 |
haftmann |
stripped class recpower further
|
file |
diff |
annotate
|
| 2009-04-15 |
haftmann |
theory NatBin now named Nat_Numeral
|
file |
diff |
annotate
|
| 2009-04-05 |
chaieb |
More precise treatement of rational constants by the normalizer for fields
|
file |
diff |
annotate
|
| 2009-04-05 |
chaieb |
now deals with devision in fields
|
file |
diff |
annotate
|
| 2009-03-26 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| 2009-03-22 |
haftmann |
dropped theory Arith_Tools
|
file |
diff |
annotate
|
| 2009-03-16 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| 2009-03-13 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| 2009-03-04 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| 2009-03-04 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| 2009-02-24 |
huffman |
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
|
file |
diff |
annotate
|
| 2009-02-21 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
| 2009-02-21 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|