| Sat, 10 Jan 2009 01:28:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 10 Jan 2009 01:28:03 +0100 |
wenzelm |
added force_result;
|
changeset |
files
|
| Sat, 10 Jan 2009 00:25:31 +0100 |
wenzelm |
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
|
changeset |
files
|
| Sat, 10 Jan 2009 00:24:07 +0100 |
wenzelm |
simplified join_proofs;
|
changeset |
files
|
| Fri, 09 Jan 2009 23:39:53 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 09 Jan 2009 23:34:36 +0100 |
wenzelm |
added split_thy_path;
|
changeset |
files
|
| Fri, 09 Jan 2009 23:33:59 +0100 |
wenzelm |
added running task markup;
|
changeset |
files
|
| Thu, 08 Jan 2009 13:18:34 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 08 Jan 2009 12:15:23 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 09 Jan 2009 19:41:33 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 09 Jan 2009 09:49:01 -0800 |
huffman |
merged.
|
changeset |
files
|
| Fri, 09 Jan 2009 09:34:49 -0800 |
huffman |
fix proof broken by changes in dvd theory
|
changeset |
files
|
| Thu, 08 Jan 2009 21:13:40 -0800 |
huffman |
merged.
|
changeset |
files
|
| Thu, 08 Jan 2009 12:25:22 -0800 |
huffman |
remove type-specific proofs
|
changeset |
files
|
| Thu, 08 Jan 2009 10:43:09 -0800 |
huffman |
add lemma dvd_diff to class comm_ring_1
|
changeset |
files
|
| Thu, 08 Jan 2009 10:26:50 -0800 |
huffman |
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
|
changeset |
files
|
| Thu, 08 Jan 2009 10:07:39 -0800 |
huffman |
move lemmas mult_minus{left,right} inside class ring
|
changeset |
files
|
| Thu, 08 Jan 2009 09:58:36 -0800 |
huffman |
clean up division_ring proofs
|
changeset |
files
|
| Thu, 08 Jan 2009 09:12:29 -0800 |
huffman |
add class ring_div; generalize mod/diff/minus proofs for class ring_div
|
changeset |
files
|
| Thu, 08 Jan 2009 08:36:16 -0800 |
huffman |
generalize zmod_zmod_cancel -> mod_mod_cancel
|
changeset |
files
|
| Thu, 08 Jan 2009 08:24:08 -0800 |
huffman |
generalize some div/mod lemmas; remove type-specific proofs
|
changeset |
files
|
| Wed, 07 Jan 2009 08:13:56 -0800 |
huffman |
add tracing for domain package proofs
|
changeset |
files
|
| Tue, 06 Jan 2009 11:49:23 -0800 |
huffman |
rename abbreviation square -> power2, to match theorem names
|
changeset |
files
|
| Fri, 09 Jan 2009 08:22:44 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 08 Jan 2009 17:10:41 +0100 |
haftmann |
split of Imperative_HOL theories from HOL-Library
|
changeset |
files
|
| Thu, 08 Jan 2009 17:25:06 +0100 |
haftmann |
NEWS and CONTRIBUTORS
|
changeset |
files
|
| Thu, 08 Jan 2009 10:53:48 +0100 |
haftmann |
dded code_thm antiquotation
|
changeset |
files
|
| Thu, 08 Jan 2009 08:06:11 +0100 |
haftmann |
made SML/NJ happy
|
changeset |
files
|