| Sat, 27 Aug 2011 16:01:24 +0200 |
wenzelm |
tuned colors;
|
changeset |
files
|
| Sat, 27 Aug 2011 15:53:18 +0200 |
wenzelm |
transparent foreground color for quoted entities;
|
changeset |
files
|
| Sat, 27 Aug 2011 13:26:06 +0200 |
wenzelm |
more precise treatment of nodes that are fully required for partially visible ones;
|
changeset |
files
|
| Sat, 27 Aug 2011 12:22:24 +0200 |
wenzelm |
de-assigned commands also count as changed;
|
changeset |
files
|
| Sat, 27 Aug 2011 11:22:21 +0200 |
blanchet |
beef up sledgehammer_tac in Mirabelle some more
|
changeset |
files
|
| Sat, 27 Aug 2011 11:22:11 +0200 |
blanchet |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 21:52:11 +0200 |
blanchet |
change default for generation of tag idempotence and tag argument equations
|
changeset |
files
|
| Fri, 26 Aug 2011 15:11:33 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 15:11:26 -0700 |
huffman |
NEWS entry for setsum_norm ~> norm_setsum
|
changeset |
files
|
| Fri, 26 Aug 2011 15:00:00 -0700 |
huffman |
make HOL-Probability respect set/pred distinction
|
changeset |
files
|
| Fri, 26 Aug 2011 23:14:36 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 08 Sep 2010 16:10:49 -0700 |
huffman |
use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
|
changeset |
files
|
| Fri, 26 Aug 2011 10:38:29 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 08:56:29 -0700 |
huffman |
generalize and simplify proof of continuous_within_sequentially
|
changeset |
files
|
| Fri, 26 Aug 2011 08:12:38 -0700 |
huffman |
add lemma sequentially_imp_eventually_within;
|
changeset |
files
|