#
caa31cef |
|
22-Jun-2019 |
haftmann <none@none> |
streamlined setup for linear algebra, particularly removed redundant rule declarations
|
#
da27d24f |
|
14-Jun-2019 |
haftmann <none@none> |
moved some theorems into HOL main corpus
|
#
a1c1e852 |
|
14-Jun-2019 |
haftmann <none@none> |
official fact collection sign_simps
|
#
6f3e8c54 |
|
14-Jun-2019 |
haftmann <none@none> |
avoid pseudo-collection to be used in generated proofs
|
#
7b38a052 |
|
14-Jun-2019 |
haftmann <none@none> |
moved comment to approproiate place
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
14f1ca5d |
|
28-Jun-2018 |
wenzelm <none@none> |
avoid pending shyps in global theory facts;
|
#
05d25f5b |
|
28-Jun-2018 |
nipkow <none@none> |
added lemmas
|
#
96a39121 |
|
14-Jun-2018 |
nipkow <none@none> |
removed duplicates
|
#
85b3e948 |
|
11-Nov-2017 |
haftmann <none@none> |
dedicated definition for coprimality --HG-- extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae
|
#
2ef94418 |
|
08-Oct-2017 |
haftmann <none@none> |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel --HG-- extra : rebase_source : c6612d6016d811043143eafb7a671631287494a1
|
#
3f30d088 |
|
22-Apr-2017 |
wenzelm <none@none> |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications; --HG-- rename : src/HOL/Main.thy => src/HOL/Pre_Main.thy
|
#
715daca5 |
|
09-Jan-2017 |
haftmann <none@none> |
moved some lemmas to appropriate places --HG-- extra : rebase_source : d3d8537b1c25edc3e07620dda770ad1feb37ea72
|
#
46c06843 |
|
03-Jan-2017 |
paulson <lp15@cam.ac.uk> |
A few new lemmas and needed adaptations
|
#
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
#
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
#
7cb68da2 |
|
16-Oct-2016 |
haftmann <none@none> |
more standardized names
|
#
cb102454 |
|
18-Sep-2016 |
wenzelm <none@none> |
tuned proofs;
|
#
4a35a4bd |
|
17-Aug-2016 |
boehmes <none@none> |
more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay
|
#
b7ba6e77 |
|
15-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
c9ad5b19 |
|
14-Jul-2016 |
eberlm <eberlm@in.tum.de> |
Tuned looping simp rules in semiring_div --HG-- extra : rebase_source : 3b3829fdddfdfffaad7cac785a601ef678dc9b93
|
#
2e12e903 |
|
20-Jun-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
e3b38c13 |
|
17-Feb-2016 |
haftmann <none@none> |
dropped various legacy fact bindings
|
#
227dc99e |
|
06-Jan-2016 |
blanchet <none@none> |
more complete setup for 'Rat' in Nitpick
|
#
08cabf03 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "abs";
|
#
ecc07c37 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "floor", "ceiling";
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
e0a30cbb |
|
09-Sep-2015 |
wenzelm <none@none> |
simplified simproc programming interfaces;
|
#
78ffd573 |
|
31-Aug-2015 |
wenzelm <none@none> |
prefer symbols;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
81da5767 |
|
08-Jul-2015 |
haftmann <none@none> |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
#
603f8dfb |
|
12-Jun-2015 |
haftmann <none@none> |
uniform _ div _ as infix syntax for ring division --HG-- extra : rebase_source : c4a1892078772c7ce9af33ad66e2abfefe7adea9
|
#
f2ba2c03 |
|
01-Jun-2015 |
haftmann <none@none> |
separate class for division operator, with particular syntax added in more specific classes
|
#
9fdf6e80 |
|
09-Apr-2015 |
haftmann <none@none> |
conversion between division on nat/int and division in archmedean fields
|
#
ac517014 |
|
31-Mar-2015 |
haftmann <none@none> |
given up separate type classes demanding `inverse 0 = 0`
|
#
08ee2a04 |
|
10-Mar-2015 |
paulson <lp15@cam.ac.uk> |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
#
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
dc5a029e |
|
30-Oct-2014 |
haftmann <none@none> |
more simp rules concerning dvd and even/odd --HG-- extra : rebase_source : 895ed3f871c22790e8d199a30828e91bc13bd735
|
#
6a02610c |
|
21-Sep-2014 |
haftmann <none@none> |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
#
a5771a76 |
|
19-Jul-2014 |
haftmann <none@none> |
more appropriate postprocessing of rational numbers: extract sign to front of fraction
|
#
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
#
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
#
58c27ade |
|
17-Jun-2014 |
hoelzl <none@none> |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin --HG-- extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2
|
#
0346c0ce |
|
30-May-2014 |
nipkow <none@none> |
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
|
#
66804330 |
|
14-Apr-2014 |
hoelzl <none@none> |
added divide_nonneg_nonneg and co; made it a simp rule --HG-- extra : rebase_source : 998eadb7cfbf8720cf961ac2e149ce4537557a47
|
#
5723122d |
|
12-Apr-2014 |
nipkow <none@none> |
made mult_pos_pos a simp rule
|
#
77b90a1d |
|
09-Apr-2014 |
hoelzl <none@none> |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
#
36a1e2cc |
|
03-Apr-2014 |
paulson <lp15@cam.ac.uk> |
removing simprule status for divide_minus_left and divide_minus_right
|
#
acab6ad5 |
|
07-Mar-2014 |
wenzelm <none@none> |
more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
|
#
b96e01d8 |
|
25-Jan-2014 |
wenzelm <none@none> |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
#
ac866a0f |
|
25-Dec-2013 |
haftmann <none@none> |
prefer more canonical names for lemmas on min/max
|
#
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
#
685750d1 |
|
12-Nov-2013 |
hoelzl <none@none> |
support of_rat with 0 or 1 on order relations
|
#
d2ef840a |
|
01-Nov-2013 |
haftmann <none@none> |
more simplification rules on unary and binary minus --HG-- extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1
|
#
837093ba |
|
16-Sep-2013 |
kuncar <none@none> |
use lifting_forget for deregistering numeric types as a quotient type
|
#
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
#
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
#
61e69372 |
|
13-Aug-2013 |
kuncar <none@none> |
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
|
#
48172fd4 |
|
25-May-2013 |
wenzelm <none@none> |
tuned;
|
#
8c36fedb |
|
13-May-2013 |
kuncar <none@none> |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
#
2597c77d |
|
19-Feb-2013 |
kuncar <none@none> |
delete also predicates on relations when hiding an implementation of an abstract type
|
#
5a8927d0 |
|
15-Feb-2013 |
haftmann <none@none> |
two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one --HG-- extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17
|
#
8e65386b |
|
14-Feb-2013 |
haftmann <none@none> |
reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck --HG-- rename : src/HOL/DSequence.thy => src/HOL/Limited_Sequence.thy rename : src/HOL/Quickcheck.thy => src/HOL/Quickcheck_Random.thy extra : rebase_source : b6adaac1637d6d1cc809d2f937ae890fcc21969c
|
#
b1299409 |
|
23-Nov-2012 |
hoelzl <none@none> |
add quotient_of_div --HG-- extra : rebase_source : 6927ab046fdc2bf74173dc2e2b5f06fc5e3c2897
|
#
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
a4d6bf89 |
|
21-May-2012 |
kuncar <none@none> |
use quot_del instead of ML code in Rat.thy
|
#
d5fef389 |
|
10-May-2012 |
huffman <none@none> |
simplify instance proofs for rat --HG-- extra : transplant_source : %A4%AC%BA%89%85%90%97%16%EDf%13L%3B3%A7%AE%89%A8p%07
|
#
37ad3d70 |
|
10-May-2012 |
huffman <none@none> |
convert Rat.thy to use lift_definition/transfer
|
#
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
#
16a2ce8b |
|
02-Mar-2012 |
bulwahn <none@none> |
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
|
#
73beb7c3 |
|
12-Dec-2011 |
bulwahn <none@none> |
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
|
#
d8e74f87 |
|
30-Nov-2011 |
wenzelm <none@none> |
prefer typedef without extra definition and alternative name; tuned proofs;
|
#
1ffaa375 |
|
15-Nov-2011 |
bulwahn <none@none> |
improved generators for rational numbers to generate negative numbers; added examples
|
#
75e76e47 |
|
13-Nov-2011 |
blanchet <none@none> |
remove unsound line in Nitpick's "rat" setup
|
#
6c2b2a7c |
|
19-Oct-2011 |
bulwahn <none@none> |
removing old code generator setup for rational numbers; tuned
|
#
da970ac6 |
|
18-Jul-2011 |
bulwahn <none@none> |
adding code equations for partial_term_of for rational numbers
|
#
e0616246 |
|
18-Jul-2011 |
bulwahn <none@none> |
adding narrowing instances for real and rational
|
#
29f8fb3e |
|
09-Jul-2011 |
bulwahn <none@none> |
adding code equations to execute floor and ceiling on rational and real numbers
|
#
4f5acb61 |
|
09-Jul-2011 |
bulwahn <none@none> |
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
|
#
4322b136 |
|
08-Apr-2011 |
bulwahn <none@none> |
rational and real instances for new compilation scheme for exhaustive quickcheck
|
#
8284061e |
|
11-Mar-2011 |
bulwahn <none@none> |
moving exhaustive_generators.ML to Quickcheck directory --HG-- rename : src/HOL/Tools/exhaustive_generators.ML => src/HOL/Tools/Quickcheck/exhaustive_generators.ML
|
#
47bb2a89 |
|
21-Feb-2011 |
blanchet <none@none> |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
#
fa3c0522 |
|
16-Dec-2010 |
bulwahn <none@none> |
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
|
#
56826ded |
|
30-Nov-2010 |
haftmann <none@none> |
adapted proofs to slightly changed definitions of congruent(2)
|
#
ba56a1d0 |
|
29-Nov-2010 |
haftmann <none@none> |
replaced slightly odd locale congruent by plain definition
|
#
18b15cec |
|
29-Nov-2010 |
haftmann <none@none> |
equivI has replaced equiv.intro
|
#
0bb01cdc |
|
01-Oct-2010 |
haftmann <none@none> |
constant `contents` renamed to `the_elem`
|
#
972f5d58 |
|
27-Aug-2010 |
haftmann <none@none> |
renamed class/constant eq to equal; tuned some instantiations
|
#
1489eccf |
|
08-Aug-2010 |
blanchet <none@none> |
replace "setup" with "declaration"
|
#
56da0db8 |
|
06-Aug-2010 |
blanchet <none@none> |
adapt occurrences of renamed Nitpick functions
|
#
8c105c87 |
|
09-Jul-2010 |
haftmann <none@none> |
nicer xsymbol syntax for fcomp and scomp
|
#
557987a9 |
|
11-Jun-2010 |
blanchet <none@none> |
adjust Nitpick's handling of "<" on "rat"s and "reals"
|
#
e3a0b01e |
|
27-May-2010 |
wenzelm <none@none> |
constant Rat.normalize needs to be qualified;
|
#
0baab8cf |
|
27-Apr-2010 |
haftmann <none@none> |
explicit is better than implicit
|
#
756c3e6e |
|
26-Apr-2010 |
haftmann <none@none> |
use new classes (linordered_)field_inverse_zero
|
#
f2a891d4 |
|
26-Apr-2010 |
haftmann <none@none> |
class division_ring_inverse_zero
|
#
18670e55 |
|
23-Apr-2010 |
haftmann <none@none> |
separated instantiation of division_by_zero
|
#
8572c6f7 |
|
11-Apr-2010 |
haftmann <none@none> |
user interface for abstract datatypes is an attribute, not a command
|
#
6fe63862 |
|
11-Mar-2010 |
haftmann <none@none> |
tuned prefixes of ac interpretations
|
#
5e512ec7 |
|
27-Feb-2010 |
wenzelm <none@none> |
clarified @{const_name} vs. @{const_abbrev};
|
#
8ad51fb8 |
|
26-Feb-2010 |
haftmann <none@none> |
implement quotient_of for odl SML code generator
|
#
8cf8d6b1 |
|
24-Feb-2010 |
haftmann <none@none> |
bound argument for abstype proposition
|
#
f3f59d7e |
|
24-Feb-2010 |
haftmann <none@none> |
renamed theory Rational to Rat --HG-- rename : src/HOL/Rational.thy => src/HOL/Rat.thy
|