#
5c168cf9 |
|
14-Jun-2019 |
haftmann <none@none> |
avoid spammed sledgehammer proofs
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
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
|