| Fri, 29 Jun 2018 22:14:33 +0200 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 21:05:56 +0200 |
wenzelm |
avoid pending shyps in global theory facts;
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 17:14:52 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Thu, 14 Jun 2018 10:51:12 +0200 |
nipkow |
removed duplicates
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 18:53:20 +0100 |
haftmann |
moved some lemmas to appropriate places
|
file |
diff |
annotate
|
| Tue, 03 Jan 2017 16:48:49 +0000 |
paulson |
A few new lemmas and needed adaptations
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 16:59:15 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2016 10:23:49 +0200 |
boehmes |
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
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 12:24:04 +0200 |
eberlm |
Merged
|
file |
diff |
annotate
|
| Thu, 14 Jul 2016 14:43:09 +0200 |
eberlm |
Tuned looping simp rules in semiring_div
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 11:07:51 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2016 22:30:23 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 13:04:30 +0100 |
blanchet |
more complete setup for 'Rat' in Nitpick
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:26:34 +0100 |
wenzelm |
prefer symbols for "abs";
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 21:46:36 +0100 |
wenzelm |
prefer symbols for "floor", "ceiling";
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 21:28:08 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 14:01:41 +0200 |
haftmann |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
file |
diff |
annotate
|
| Fri, 12 Jun 2015 08:53:23 +0200 |
haftmann |
uniform _ div _ as infix syntax for ring division
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 09:12:47 +0200 |
haftmann |
conversion between division on nat/int and division in archmedean fields
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 15:20:40 +0000 |
paulson |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 21:02:01 +0100 |
haftmann |
more simp rules concerning dvd and even/odd
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
| Sat, 19 Jul 2014 18:30:42 +0200 |
haftmann |
more appropriate postprocessing of rational numbers: extract sign to front of fraction
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 07:31:12 +0200 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
| Fri, 30 May 2014 18:13:40 +0200 |
nipkow |
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
|
file |
diff |
annotate
|
| Mon, 14 Apr 2014 13:08:17 +0200 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 23:51:52 +0100 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 11:46:26 +0100 |
wenzelm |
more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 22:06:07 +0100 |
wenzelm |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:51 +0100 |
hoelzl |
support of_rat with 0 or 1 on order relations
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 15:30:20 +0200 |
kuncar |
use lifting_forget for deregistering numeric types as a quotient type
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 17:45:22 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
|
file |
diff |
annotate
|
| Sat, 25 May 2013 17:13:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 13 May 2013 13:59:04 +0200 |
kuncar |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 15:03:36 +0100 |
kuncar |
delete also predicates on relations when hiding an implementation of an abstract type
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 15:27:10 +0100 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
| Fri, 23 Nov 2012 18:28:00 +0100 |
hoelzl |
add quotient_of_div
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Mon, 21 May 2012 16:37:28 +0200 |
kuncar |
use quot_del instead of ML code in Rat.thy
|
file |
diff |
annotate
|
| Thu, 10 May 2012 21:02:36 +0200 |
huffman |
simplify instance proofs for rat
|
file |
diff |
annotate
|
| Thu, 10 May 2012 21:18:41 +0200 |
huffman |
convert Rat.thy to use lift_definition/transfer
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Fri, 02 Mar 2012 09:35:35 +0100 |
bulwahn |
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 13:45:54 +0100 |
bulwahn |
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 15:38:50 +0100 |
bulwahn |
improved generators for rational numbers to generate negative numbers;
|
file |
diff |
annotate
|
| Sun, 13 Nov 2011 20:28:22 +0100 |
blanchet |
remove unsound line in Nitpick's "rat" setup
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 09:11:14 +0200 |
bulwahn |
removing old code generator setup for rational numbers; tuned
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adding code equations for partial_term_of for rational numbers
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adding narrowing instances for real and rational
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 19:28:33 +0200 |
bulwahn |
adding code equations to execute floor and ceiling on rational and real numbers
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 13:41:58 +0200 |
bulwahn |
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
rational and real instances for new compilation scheme for exhaustive quickcheck
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
moving exhaustive_generators.ML to Quickcheck directory
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 12:14:18 +0100 |
bulwahn |
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
|
file |
diff |
annotate
|
| Tue, 30 Nov 2010 15:58:09 +0100 |
haftmann |
adapted proofs to slightly changed definitions of congruent(2)
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 22:32:06 +0100 |
haftmann |
replaced slightly odd locale congruent by plain definition
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 13:44:54 +0100 |
haftmann |
equivI has replaced equiv.intro
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 16:05:25 +0200 |
haftmann |
constant `contents` renamed to `the_elem`
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 12:53:16 +0200 |
blanchet |
replace "setup" with "declaration"
|
file |
diff |
annotate
|
| Fri, 06 Aug 2010 17:23:11 +0200 |
blanchet |
adapt occurrences of renamed Nitpick functions
|
file |
diff |
annotate
|
| Fri, 09 Jul 2010 08:11:10 +0200 |
haftmann |
nicer xsymbol syntax for fcomp and scomp
|
file |
diff |
annotate
|
| Fri, 11 Jun 2010 17:05:11 +0200 |
blanchet |
adjust Nitpick's handling of "<" on "rat"s and "reals"
|
file |
diff |
annotate
|
| Thu, 27 May 2010 15:15:20 +0200 |
wenzelm |
constant Rat.normalize needs to be qualified;
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 09:49:40 +0200 |
haftmann |
explicit is better than implicit
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 15:37:50 +0200 |
haftmann |
use new classes (linordered_)field_inverse_zero
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:17 +0200 |
haftmann |
class division_ring_inverse_zero
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 15:18:00 +0200 |
haftmann |
separated instantiation of division_by_zero
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 16:51:07 +0200 |
haftmann |
user interface for abstract datatypes is an attribute, not a command
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 14:39:58 +0100 |
haftmann |
tuned prefixes of ac interpretations
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 20:57:08 +0100 |
wenzelm |
clarified @{const_name} vs. @{const_abbrev};
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 10:57:35 +0100 |
haftmann |
merged
|
file |
diff |
annotate
| base
|
| Fri, 26 Feb 2010 10:48:20 +0100 |
haftmann |
implement quotient_of for odl SML code generator
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:42:28 +0100 |
haftmann |
bound argument for abstype proposition
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:34:40 +0100 |
haftmann |
renamed theory Rational to Rat
|
file |
diff |
annotate
| base
|