| Wed, 27 Aug 2008 01:27:33 +0200 |
add lemmas about Rats similar to those about Reals
|
file | diff | annotate |
| Tue, 26 Aug 2008 12:07:06 +0200 |
Defined rationals (Rats) globally in Rational.
|
file | diff | annotate |
| Fri, 25 Jul 2008 12:03:34 +0200 |
added class preorder
|
file | diff | annotate |
| Mon, 21 Jul 2008 13:36:59 +0200 |
Tuned and simplified proofs
|
file | diff | annotate |
| Fri, 18 Jul 2008 18:25:56 +0200 |
refined code generator setup for rational numbers; more simplification rules for rational numbers
|
file | diff | annotate |
| Fri, 11 Jul 2008 09:03:11 +0200 |
Fract now total; improved code generator setup
|
file | diff | annotate |
| Wed, 09 Jul 2008 20:18:06 +0200 |
rearrange instantiations
|
file | diff | annotate |
| Tue, 22 Apr 2008 08:33:16 +0200 |
constant HOL.eq now qualified
|
file | diff | annotate |
| Wed, 02 Apr 2008 15:58:32 +0200 |
explicit class "eq" for operational equality
|
file | diff | annotate |
| Fri, 25 Jan 2008 14:54:41 +0100 |
improved code theorem setup
|
file | diff | annotate |
| Thu, 10 Jan 2008 19:09:21 +0100 |
New interface for test data generators.
|
file | diff | annotate |
| Wed, 02 Jan 2008 15:14:02 +0100 |
splitted class uminus from class minus
|
file | diff | annotate |
| Fri, 07 Dec 2007 15:07:59 +0100 |
instantiation target rather than legacy instance
|
file | diff | annotate |
| Thu, 29 Nov 2007 17:08:26 +0100 |
instance command as rudimentary class target
|
file | diff | annotate |
| Thu, 20 Sep 2007 16:37:33 +0200 |
fixed cg setup
|
file | diff | annotate |
| Tue, 18 Sep 2007 16:08:00 +0200 |
simplified type int (eliminated IntInf.int, integer);
|
file | diff | annotate |
| Tue, 18 Sep 2007 07:36:13 +0200 |
renamed constructor RatC to Rational
|
file | diff | annotate |
| Thu, 06 Sep 2007 11:38:10 +0200 |
Added code generator setup (taken from Library/Executable_Rat.thy,
|
file | diff | annotate |
| Sat, 01 Sep 2007 01:21:48 +0200 |
final(?) iteration of sgn saga.
|
file | diff | annotate |
| Thu, 09 Aug 2007 15:52:53 +0200 |
adaptions for code generation
|
file | diff | annotate |
| Tue, 31 Jul 2007 00:56:26 +0200 |
arith method setup: proper context;
|
file | diff | annotate |
| Fri, 20 Jul 2007 14:28:01 +0200 |
split class abs from class minus
|
file | diff | annotate |
| Wed, 20 Jun 2007 05:06:16 +0200 |
simplify some proofs
|
file | diff | annotate |
| Wed, 13 Jun 2007 03:31:11 +0200 |
removed constant int :: nat => int;
|
file | diff | annotate |
| Tue, 12 Jun 2007 17:20:30 +0200 |
more of_rat lemmas
|
file | diff | annotate |
| Tue, 12 Jun 2007 17:04:26 +0200 |
add function of_rat and related lemmas
|
file | diff | annotate |
| Fri, 16 Mar 2007 21:32:12 +0100 |
added lattice definitions
|
file | diff | annotate |
| Fri, 17 Nov 2006 02:20:03 +0100 |
more robust syntax for definition/abbreviation/notation;
|
file | diff | annotate |
| Wed, 13 Sep 2006 00:38:38 +0200 |
added instance rat :: recpower
|
file | diff | annotate |
| Wed, 06 Sep 2006 13:48:02 +0200 |
got rid of Numeral.bin type
|
file | diff | annotate |
| Fri, 02 Jun 2006 23:22:29 +0200 |
misc cleanup;
|
file | diff | annotate |
| Thu, 09 Feb 2006 03:34:56 +0100 |
removed redundant lemmas
|
file | diff | annotate |
| Thu, 09 Feb 2006 03:01:11 +0100 |
no longer need All_equiv lemmas
|
file | diff | annotate |
| Thu, 02 Feb 2006 19:57:13 +0100 |
reimplemented using Equiv_Relations.thy
|
file | diff | annotate |
| Thu, 08 Dec 2005 20:15:50 +0100 |
tuned proofs;
|
file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 |
migrated theory headers to new format
|
file | diff | annotate |
| Wed, 18 Aug 2004 11:09:40 +0200 |
import -> imports
|
file | diff | annotate |
| Mon, 16 Aug 2004 14:22:27 +0200 |
New theory header syntax.
|
file | diff | annotate |
| Thu, 01 Jul 2004 12:29:53 +0200 |
new treatment of binary numerals
|
file | diff | annotate |
| Mon, 21 Jun 2004 10:25:57 +0200 |
Merged in license change from Isabelle2004
|
file | diff | annotate |
| Sat, 01 May 2004 22:01:57 +0200 |
tuned instance statements;
|
file | diff | annotate |
| Thu, 04 Mar 2004 12:06:07 +0100 |
new material from Avigad, and simplified treatment of division by 0
|
file | diff | annotate |
| Mon, 01 Mar 2004 13:51:21 +0100 |
new Ring_and_Field hierarchy, eliminating redundant axioms
|
file | diff | annotate |
| Sun, 15 Feb 2004 10:46:37 +0100 |
Polymorphic treatment of binary arithmetic using axclasses
|
file | diff | annotate |
| Tue, 10 Feb 2004 12:02:11 +0100 |
generic of_nat and of_int functions, and generalization of iszero
|
file | diff | annotate |
| Tue, 27 Jan 2004 15:39:51 +0100 |
replacing HOL/Real/PRat, PNat by the rational number development
|
file | diff | annotate |