| Tue, 09 Nov 2010 11:17:15 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 08 Nov 2010 23:02:20 +0100 |
krauss |
removed type-inference-like behaviour from relation_tac completely; tuned
|
changeset |
files
|
| Mon, 08 Nov 2010 20:55:27 +0100 |
wenzelm |
avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
|
changeset |
files
|
| Mon, 08 Nov 2010 20:50:56 +0100 |
wenzelm |
explicitly check uniqueness of symbol recoding;
|
changeset |
files
|
| Mon, 08 Nov 2010 17:44:47 +0100 |
wenzelm |
more hints on building and running Isabelle/jEdit from command line;
|
changeset |
files
|
| Mon, 08 Nov 2010 14:41:11 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 08 Nov 2010 14:33:54 +0100 |
blanchet |
merge
|
changeset |
files
|
| Mon, 08 Nov 2010 14:33:30 +0100 |
blanchet |
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
|
changeset |
files
|
| Mon, 08 Nov 2010 05:07:18 -0800 |
huffman |
merged
|
changeset |
files
|
| Sat, 06 Nov 2010 10:01:00 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 05 Nov 2010 15:15:28 -0700 |
huffman |
(infixl "<<" 55) -> (infix "<<" 50)
|
changeset |
files
|
| Wed, 03 Nov 2010 17:22:25 -0700 |
huffman |
simplify some proofs
|
changeset |
files
|
| Wed, 03 Nov 2010 17:06:21 -0700 |
huffman |
remove unnecessary stuff from Discrete.thy
|
changeset |
files
|
| Wed, 03 Nov 2010 16:39:23 -0700 |
huffman |
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
|
changeset |
files
|
| Wed, 03 Nov 2010 15:57:39 -0700 |
huffman |
add lemma eq_imp_below
|
changeset |
files
|