Fri, 20 Oct 2017 07:46:10 +0200 |
haftmann |
added lemmas and tuned proofs
|
file |
diff |
annotate
|
Mon, 09 Oct 2017 19:10:48 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
euclidean rings need no normalization
|
file |
diff |
annotate
|
Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
more fundamental definition of div and mod on int
|
file |
diff |
annotate
|
Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
one uniform type class for parity structures
|
file |
diff |
annotate
|
Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
generalized some rules
|
file |
diff |
annotate
|
Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
generalized simproc
|
file |
diff |
annotate
|
Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
elementary definition of division on natural numbers
|
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
|
Sun, 08 Oct 2017 22:28:20 +0200 |
haftmann |
avoid fact name clashes
|
file |
diff |
annotate
|
Sun, 08 Oct 2017 22:28:19 +0200 |
haftmann |
spelling and tuned whitespace
|
file |
diff |
annotate
|
Fri, 08 Sep 2017 00:02:33 +0200 |
blanchet |
speed up proofs slightly
|
file |
diff |
annotate
|
Sun, 23 Apr 2017 14:53:35 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
Mon, 09 Jan 2017 18:53:06 +0100 |
haftmann |
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
|
file |
diff |
annotate
|
Wed, 04 Jan 2017 21:28:29 +0100 |
haftmann |
moved euclidean ring to HOL
|
file |
diff |
annotate
|
Sat, 31 Dec 2016 08:12:31 +0100 |
haftmann |
more elementary rules about div / mod on int
|
file |
diff |
annotate
|
Thu, 22 Dec 2016 10:42:08 +0100 |
haftmann |
more uniform div/mod relations
|
file |
diff |
annotate
|
Tue, 20 Dec 2016 15:39:13 +0100 |
haftmann |
emphasize dedicated rewrite rules for congruences
|
file |
diff |
annotate
|
Sat, 17 Dec 2016 15:22:14 +0100 |
haftmann |
reoriented congruence rules in non-explosive direction
|
file |
diff |
annotate
|
Sat, 17 Dec 2016 15:22:14 +0100 |
haftmann |
more fine-grained type class hierarchy for div and mod
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 13:47:37 +0200 |
haftmann |
clarified prover-specific rules
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:06 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
clarified theorem names
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
more standardized theorem names for facts involving the div and mod identity
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:03 +0200 |
haftmann |
de-orphanized declaration
|
file |
diff |
annotate
|
Wed, 12 Oct 2016 20:38:47 +0200 |
haftmann |
separate type class for arbitrary quotient and remainder partitions
|
file |
diff |
annotate
|
Mon, 03 Oct 2016 14:34:32 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|