| 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
|