| Fri, 02 Dec 2005 16:05:12 +0100 |
haftmann |
adjusted to improved code generator interface
|
file |
diff |
annotate
|
| Tue, 22 Nov 2005 12:59:25 +0100 |
haftmann |
added codegenerator
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 09:13:22 +0100 |
haftmann |
(fix for accidental commit)
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 09:12:02 +0100 |
haftmann |
(codegen)
|
file |
diff |
annotate
|
| Tue, 27 Sep 2005 12:14:39 +0200 |
berghofe |
Inserted clause for nat in number_of_codegen again ("code unfold" turned
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 12:02:56 +0200 |
berghofe |
Simplified code generator for numerals.
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:24 +0200 |
wenzelm |
added quickcheck_params (from Main.thy);
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 18:53:11 +0200 |
paulson |
more simprules now have names
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 11:51:31 +0200 |
berghofe |
Auxiliary functions to be used in generated code are now defined using "attach".
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 14:08:53 +0200 |
berghofe |
Moved code generator setup from NatBin to IntDef.
|
file |
diff |
annotate
|
| Thu, 16 Jun 2005 19:51:04 +0200 |
paulson |
a few new integer lemmas
|
file |
diff |
annotate
|
| Wed, 04 May 2005 08:36:10 +0200 |
nipkow |
Fixing a problem with lin.arith.
|
file |
diff |
annotate
|
| Wed, 02 Mar 2005 10:02:21 +0100 |
paulson |
new lemmas int_diff_cases
|
file |
diff |
annotate
|
| Tue, 01 Mar 2005 18:48:52 +0100 |
nipkow |
integrated Jeremy's FiniteLib
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:57:45 +0100 |
nipkow |
removed superfluous setsum_constant
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Wed, 15 Dec 2004 17:32:40 +0100 |
paulson |
removal of archaic Abs/Rep proofs
|
file |
diff |
annotate
|
| Tue, 14 Dec 2004 10:45:16 +0100 |
paulson |
new and stronger lemmas and improved simplification for finite sets
|
file |
diff |
annotate
|
| Fri, 19 Nov 2004 17:31:49 +0100 |
paulson |
moved and renamed Integ/Equiv.thy
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Wed, 01 Sep 2004 15:04:01 +0200 |
paulson |
new "respects" syntax for quotienting
|
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, 15 Jul 2004 15:32:32 +0200 |
paulson |
redefining sumr to be a translation to setsum
|
file |
diff |
annotate
|
| Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
| Thu, 24 Jun 2004 17:52:02 +0200 |
paulson |
replaced monomorphic abs definitions by abs_if
|
file |
diff |
annotate
|
| Wed, 12 May 2004 10:00:56 +0200 |
nipkow |
fixed latex problems
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Sat, 01 May 2004 22:01:57 +0200 |
wenzelm |
tuned instance statements;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2004 11:04:07 +0200 |
paulson |
congruent2 now allows different equiv relations
|
file |
diff |
annotate
|
| Thu, 08 Apr 2004 15:14:33 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Tue, 30 Mar 2004 11:18:12 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Thu, 25 Mar 2004 10:32:21 +0100 |
paulson |
new material from Avigad
|
file |
diff |
annotate
|
| Wed, 24 Mar 2004 10:50:29 +0100 |
paulson |
streamlined treatment of quotients for the integers
|
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
|
| Mon, 01 Mar 2004 13:51:21 +0100 |
paulson |
new Ring_and_Field hierarchy, eliminating redundant axioms
|
file |
diff |
annotate
|
| Thu, 19 Feb 2004 15:57:34 +0100 |
ballarin |
Efficient, graph-based reasoner for linear and partial orders.
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Tue, 10 Feb 2004 12:02:11 +0100 |
paulson |
generic of_nat and of_int functions, and generalization of iszero
|
file |
diff |
annotate
|
| Fri, 09 Jan 2004 10:46:18 +0100 |
paulson |
Defining the type class "ringpower" and deleting superseded theorems for
|
file |
diff |
annotate
|
| Tue, 06 Jan 2004 10:40:15 +0100 |
paulson |
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
|
file |
diff |
annotate
|
| Wed, 03 Dec 2003 10:49:34 +0100 |
paulson |
Simplification of the development of Integers
|
file |
diff |
annotate
|
| Fri, 28 Nov 2003 12:09:37 +0100 |
paulson |
conversion of some Real theories to Isar scripts
|
file |
diff |
annotate
|
| Tue, 18 Nov 2003 11:01:52 +0100 |
paulson |
conversion of ML to Isar scripts
|
file |
diff |
annotate
|
| Thu, 08 Aug 2002 23:52:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Mon, 08 Oct 2001 15:23:20 +0200 |
wenzelm |
sane numerals (stage 3): provide generic "1" on all number types;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Wed, 25 Jul 2001 13:13:01 +0200 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:32:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 18:48:18 +0100 |
nipkow |
^^ -> ```
|
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, 19 Jul 2000 12:33:36 +0200 |
paulson |
changed / to // for quotienting
|
file |
diff |
annotate
|
| Tue, 23 May 2000 18:14:57 +0200 |
paulson |
defining 0::int to be (int 0)
|
file |
diff |
annotate
|
| Fri, 27 Aug 1999 15:42:10 +0200 |
paulson |
tidied, allowing pattern-matching in defs of zadd and zmult
|
file |
diff |
annotate
|
| Thu, 29 Jul 1999 12:44:57 +0200 |
paulson |
added parentheses to cope with a possible reduction of the precedence of unary
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:27:17 +0200 |
paulson |
much tidying
|
file |
diff |
annotate
|