| Wed, 15 Apr 2009 15:30:37 +0200 |
haftmann |
more coherent developement in Divides.thy and IntDiv.thy
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 18:41:15 +0200 |
nipkow |
added nat_div_gt_0 [simp]
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 16:03:00 +0200 |
nipkow |
added strong_setprod_cong[cong] (in analogy with setsum)
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:46:11 +0100 |
haftmann |
lemma nat_dvd_not_less moved here from Arith_Tools
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 23:01:25 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 18:01:26 +0100 |
haftmann |
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 15:31:26 +0100 |
nipkow |
added div lemmas
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 17:05:18 +0100 |
nipkow |
removed and renamed redundant lemmas
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 10:24:57 +0100 |
nipkow |
added lemmas by Jeremy Avigad
|
file |
diff |
annotate
|
| Mon, 23 Feb 2009 16:25:52 -0800 |
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
|
| Mon, 23 Feb 2009 13:55:36 -0800 |
huffman |
move lemma dvd_mod_imp_dvd into class semiring_div
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 11:30:41 +0100 |
nipkow |
added dvd_div_mult
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 20:50:49 +0100 |
nipkow |
removed subsumed lemmas
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 10:24:48 -0800 |
huffman |
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 18:48:17 +0100 |
nipkow |
Cleaned up IntDiv and removed subsumed lemmas.
|
file |
diff |
annotate
|
| Sun, 15 Feb 2009 22:58:02 +0100 |
nipkow |
dvd and setprod lemmas
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 14:58:11 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 09:12:29 -0800 |
huffman |
add class ring_div; generalize mod/diff/minus proofs for class ring_div
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 08:36:16 -0800 |
huffman |
generalize zmod_zmod_cancel -> mod_mod_cancel
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 08:24:08 -0800 |
huffman |
generalize some div/mod lemmas; remove type-specific proofs
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 08:56:02 +0100 |
nipkow |
codegen
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:08 +0200 |
wenzelm |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file |
diff |
annotate
|
| Mon, 21 Jul 2008 15:27:23 +0200 |
haftmann |
(re-)added simp rules for (_ + _) div/mod _
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 09:02:22 +0200 |
haftmann |
separate class dvd for divisibility predicate
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:37:00 +0100 |
wenzelm |
removed duplicate lemmas;
|
file |
diff |
annotate
|
| Wed, 20 Feb 2008 14:52:34 +0100 |
haftmann |
using only an relation predicate to construct div and mod
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 16:09:12 +0100 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
| Wed, 13 Feb 2008 09:35:31 +0100 |
haftmann |
more abstract lemmas
|
file |
diff |
annotate
|
| Wed, 23 Jan 2008 22:57:09 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 22 Jan 2008 23:07:21 +0100 |
haftmann |
added class semiring_div
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:53:44 +0200 |
nipkow |
Eliminated most of the neq0_conv occurrences. As a result, many
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 12:09:33 +0200 |
chaieb |
fixed proofs
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 08:20:46 +0200 |
haftmann |
class div inherits from class times
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 23:04:27 +0200 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 15:20:45 +0200 |
haftmann |
using class target
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 09:23:10 +0200 |
haftmann |
introduced (auxiliary) class dvd_mod for more convenient code generation
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:50 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Sat, 19 May 2007 11:33:21 +0200 |
haftmann |
uniform module names for code generation
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:16 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:21:44 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:33:04 +0200 |
haftmann |
added lemmatas
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Tue, 17 Apr 2007 00:30:44 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 08:27:15 +0100 |
haftmann |
explizit "type" superclass
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:26:49 +0100 |
berghofe |
Adapted to changes in Transitive_Closure theory.
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:10:00 +0100 |
haftmann |
added OCaml code generation (without dictionaries)
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:15 +0100 |
haftmann |
div is now a class
|
file |
diff |
annotate
|
| Mon, 06 Nov 2006 16:28:31 +0100 |
haftmann |
code generator module naming improved
|
file |
diff |
annotate
|
| Wed, 20 Sep 2006 12:24:11 +0200 |
haftmann |
name shifts
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:21:43 +0200 |
haftmann |
explicit divmod algorithm for code generation
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Mon, 14 Aug 2006 13:46:06 +0200 |
haftmann |
simplified code generator setup
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 13:15:12 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:30 +0200 |
wenzelm |
simprocs: no theory argument -- use simpset context instead;
|
file |
diff |
annotate
|
| Tue, 17 Jan 2006 16:36:57 +0100 |
haftmann |
substantial improvements in code generator
|
file |
diff |
annotate
|
| Fri, 18 Nov 2005 07:13:58 +0100 |
chaieb |
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
|
file |
diff |
annotate
|
| Fri, 11 Nov 2005 00:09:37 +0100 |
huffman |
add header
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:21:49 +0200 |
wenzelm |
Provers/cancel_sums.ML: Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:03:37 +0200 |
wenzelm |
tuned theory dependencies;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 18:53:11 +0200 |
paulson |
more simprules now have names
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 15:36:28 +0200 |
paulson |
classical rules must have names for ATP integration
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 15:06:20 +0200 |
paulson |
generlization of some "nat" theorems
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Fri, 14 Jan 2005 12:00:27 +0100 |
nipkow |
made diff_less a simp rule
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 10:43:06 +0200 |
paulson |
new lemmas
|
file |
diff |
annotate
|
| Fri, 05 Mar 2004 15:26:04 +0100 |
paulson |
some new results
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
| Tue, 25 Nov 2003 10:37:03 +0100 |
paulson |
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
|
file |
diff |
annotate
|
| Fri, 26 Sep 2003 10:34:57 +0200 |
paulson |
misc tidying
|
file |
diff |
annotate
|
| Thu, 24 Jul 2003 18:23:00 +0200 |
paulson |
declarations moved from PreList.thy
|
file |
diff |
annotate
|
| Tue, 25 Mar 2003 09:56:01 +0100 |
berghofe |
New theorems split_div' and mod_div_equality'.
|
file |
diff |
annotate
|
| Fri, 23 Aug 2002 07:41:05 +0200 |
nipkow |
Added div+mod cancelling simproc
|
file |
diff |
annotate
|
| Fri, 31 May 2002 07:53:37 +0200 |
nipkow |
Now arith can deal with div/mod arbitrary nat numerals.
|
file |
diff |
annotate
|
| Wed, 15 May 2002 13:49:51 +0200 |
nipkow |
Divides.ML -> Divides_lemmas.ML
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 14:28:10 +0100 |
nipkow |
Changed priority of dvd from 70 to 50 as befits a relation.
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 11:03:31 +0100 |
paulson |
many new div and mod properties (borrowed from Integ/IntDiv)
|
file |
diff |
annotate
|
| Fri, 13 Oct 2000 08:28:21 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 12 Oct 2000 18:38:23 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 24 May 2000 18:48:22 +0200 |
paulson |
installing plus_ac0 for nat
|
file |
diff |
annotate
|
| Sun, 21 May 2000 14:49:28 +0200 |
wenzelm |
replaced {{ }} by { };
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:18:16 +0200 |
paulson |
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
|
file |
diff |
annotate
|
| Thu, 01 Jul 1999 10:33:50 +0200 |
paulson |
now div and mod are overloaded; dvd is polymorphic
|
file |
diff |
annotate
|
| Fri, 30 May 1997 15:15:57 +0200 |
paulson |
Moving div and mod from Arith to Divides
|
file |
diff |
annotate
|