| #
eda74618 |
|
09-Oct-2017 |
haftmann <none@none> |
tuned imports
--HG--
extra : rebase_source : bc9797cb892085195c2d8662a7ca3896dd1e5011
|
| #
38864224 |
|
10-Sep-2015 |
wenzelm <none@none> |
more standard local_theory operations;
eliminated slightly odd @{cpat};
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
55832464 |
|
19-Feb-2015 |
haftmann <none@none> |
establish unique preferred fact names
|
| #
eb7cb4d3 |
|
18-Feb-2015 |
haftmann <none@none> |
inlined rules to free user-space from technical names
|
| #
609893e7 |
|
18-Feb-2015 |
haftmann <none@none> |
explicit declaration allows cumulative declaration
|
| #
b2448e5a |
|
15-Feb-2015 |
haftmann <none@none> |
deleted ineffective declarations
|
| #
aa8f7e6e |
|
15-Feb-2015 |
haftmann <none@none> |
dropped unused rules
|
| #
7b519378 |
|
15-Feb-2015 |
haftmann <none@none> |
self-contained declaration attribute
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
| #
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
| #
d2ef840a |
|
01-Nov-2013 |
haftmann <none@none> |
more simplification rules on unary and binary minus
--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1
|
| #
b9bb5600 |
|
18-Aug-2013 |
wenzelm <none@none> |
more symbols;
|
| #
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
| #
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
| #
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
| #
18f3c72b |
|
23-Jul-2010 |
haftmann <none@none> |
proper subclass instead of sublocale
|
| #
353897d4 |
|
12-May-2010 |
haftmann <none@none> |
tuned proofs and fact and class names
|
| #
694846db |
|
12-May-2010 |
haftmann <none@none> |
tuned fact collection names and some proofs
|
| #
b85a53f1 |
|
11-May-2010 |
haftmann <none@none> |
grouped local statements
|
| #
dd23bb2e |
|
11-May-2010 |
hoelzl <none@none> |
Add rules directly to the corresponding class locales instead.
|
| #
6de25d5f |
|
08-May-2010 |
haftmann <none@none> |
moved normalization proof tool infrastructure to canonical algebraic classes
|
| #
c50c0636 |
|
07-May-2010 |
haftmann <none@none> |
renamed Normalizer to the more specific Semiring_Normalizer
--HG--
rename : src/HOL/Tools/Groebner_Basis/normalizer.ML => src/HOL/Tools/semiring_normalizer.ML
|
| #
91ddab8e |
|
07-May-2010 |
haftmann <none@none> |
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
--HG--
rename : src/HOL/Groebner_Basis.thy => src/HOL/Semiring_Normalization.thy
|