| Wed, 28 Jan 2009 16:57:36 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 28 Jan 2009 16:57:12 +0100 |
nipkow |
merged - resolving conflics
|
changeset |
files
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
changeset |
files
|
| Wed, 28 Jan 2009 16:35:57 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 28 Jan 2009 16:35:42 +0100 |
haftmann |
explicit check for exactly one type variable in class specification elements
|
changeset |
files
|
| Wed, 28 Jan 2009 06:03:46 -0800 |
huffman |
merged
|
changeset |
files
|
| Tue, 27 Jan 2009 22:39:41 -0800 |
huffman |
merged
|
changeset |
files
|
| Thu, 22 Jan 2009 06:42:05 -0800 |
huffman |
removed use of prev_cont_thms reference
|
changeset |
files
|
| Thu, 22 Jan 2009 06:09:41 -0800 |
huffman |
merged
|
changeset |
files
|
| Wed, 21 Jan 2009 21:01:15 -0800 |
huffman |
add lemmas about div/mod with multiplication
|
changeset |
files
|
| Wed, 21 Jan 2009 20:20:56 -0800 |
huffman |
add lemmas about smult
|
changeset |
files
|
| Wed, 28 Jan 2009 13:36:24 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 28 Jan 2009 13:36:11 +0100 |
haftmann |
slightly adapted towards more uniformity with div/mod on nat
|
changeset |
files
|
| Wed, 28 Jan 2009 11:04:45 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 28 Jan 2009 11:03:42 +0100 |
haftmann |
Plain, Main form meeting points in import hierarchy
|
changeset |
files
|
| Wed, 28 Jan 2009 11:03:16 +0100 |
haftmann |
Plain, Main form meeting points in import hierarchy
|
changeset |
files
|
| Wed, 28 Jan 2009 11:02:12 +0100 |
haftmann |
added lemma abs_sng
|
changeset |
files
|
| Wed, 28 Jan 2009 11:02:12 +0100 |
haftmann |
nat is a bot instance
|
changeset |
files
|
| Wed, 28 Jan 2009 11:02:11 +0100 |
haftmann |
slightly adapted towards more uniformity with div/mod on nat
|
changeset |
files
|
| Wed, 28 Jan 2009 11:04:10 +0100 |
haftmann |
Reflection.thy now in HOL/Library
|
changeset |
files
|
| Wed, 28 Jan 2009 11:36:45 +0100 |
wenzelm |
more robust treatment of SwingUtilities.isEventDispatchThread;
|
changeset |
files
|
| Wed, 28 Jan 2009 10:43:31 +0100 |
wenzelm |
annotate shared vars as @volatile;
|
changeset |
files
|
| Tue, 27 Jan 2009 19:56:26 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Tue, 27 Jan 2009 19:56:20 +0100 |
wenzelm |
added label;
|
changeset |
files
|
| Tue, 27 Jan 2009 15:47:22 +0100 |
wenzelm |
plain non-dependent types;
|
changeset |
files
|
| Tue, 27 Jan 2009 15:22:46 +0100 |
wenzelm |
turned IsarDocument into trait for IsabelleProcess;
|
changeset |
files
|
| Tue, 27 Jan 2009 14:45:52 +0100 |
wenzelm |
HOL_USEDIR_OPTIONS: -Q false, giving up parallel proofs for now due to memory shortage;
|
changeset |
files
|
| Tue, 27 Jan 2009 14:28:51 +0100 |
wenzelm |
thm_proof: recovered single-threaded version;
|
changeset |
files
|
| Tue, 27 Jan 2009 13:52:32 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 27 Jan 2009 13:41:45 +0100 |
wenzelm |
recovered example types from WordMain.thy;
|
changeset |
files
|