| Thu, 20 May 2010 16:22:50 +0200 |
wenzelm |
determine margin just before rendering -- proper reformatting when updating;
|
changeset |
files
|
| Thu, 20 May 2010 15:51:28 +0200 |
wenzelm |
simplified alignment via FlowPanel;
|
changeset |
files
|
| Thu, 20 May 2010 13:54:31 +0200 |
wenzelm |
more systematic treatment of physical document wrt. font size etc.;
|
changeset |
files
|
| Thu, 20 May 2010 11:44:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 20 May 2010 11:36:30 +0200 |
wenzelm |
general Isabelle_System.try_read;
|
changeset |
files
|
| Thu, 20 May 2010 10:43:46 +0200 |
wenzelm |
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
|
changeset |
files
|
| Thu, 20 May 2010 10:31:20 +0200 |
wenzelm |
inverted "Freeze" to "Follow", which is the default;
|
changeset |
files
|
| Wed, 19 May 2010 21:18:02 +0200 |
wenzelm |
basic controls to freeze/update prover results;
|
changeset |
files
|
| Wed, 19 May 2010 18:05:34 +0200 |
wenzelm |
show fully detailed protocol messages;
|
changeset |
files
|
| Wed, 19 May 2010 17:39:22 +0200 |
wenzelm |
some updates following src/Tools/jEdit/dist-template/settings;
|
changeset |
files
|
| Wed, 19 May 2010 12:35:20 +0200 |
haftmann |
spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
|
changeset |
files
|
| Wed, 19 May 2010 10:17:31 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 19 May 2010 10:17:05 +0200 |
haftmann |
dropped legacy_unconstrainT
|
changeset |
files
|
| Wed, 19 May 2010 10:14:37 +0200 |
haftmann |
new version of triv_of_class machinery without legacy_unconstrain
|
changeset |
files
|
| Wed, 19 May 2010 09:21:30 +0200 |
haftmann |
merge
|
changeset |
files
|
| Wed, 19 May 2010 09:20:36 +0200 |
haftmann |
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
|
changeset |
files
|
| Tue, 18 May 2010 19:00:55 -0700 |
huffman |
remove several redundant lemmas about floor and ceiling
|
changeset |
files
|
| Tue, 18 May 2010 06:28:42 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 17 May 2010 18:59:59 -0700 |
huffman |
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
|
changeset |
files
|
| Mon, 17 May 2010 18:51:25 -0700 |
huffman |
simplify proof
|
changeset |
files
|
| Mon, 17 May 2010 16:52:34 -0700 |
huffman |
simplify proof
|
changeset |
files
|
| Mon, 17 May 2010 15:58:32 -0700 |
huffman |
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
|
changeset |
files
|
| Tue, 18 May 2010 10:13:33 +0200 |
wenzelm |
prefer structure Keyword and Parse;
|
changeset |
files
|
| Tue, 18 May 2010 00:01:51 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 17 May 2010 12:00:10 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 17 May 2010 08:45:46 -0700 |
huffman |
remove simp attribute from square_eq_1_iff
|
changeset |
files
|
| Mon, 17 May 2010 17:50:09 +0200 |
blanchet |
merged
|
changeset |
files
|
| Mon, 17 May 2010 15:21:11 +0200 |
blanchet |
make sure chained facts don't pop up in the metis proof
|
changeset |
files
|
| Mon, 17 May 2010 12:15:37 +0200 |
blanchet |
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
|
changeset |
files
|
| Mon, 17 May 2010 10:18:14 +0200 |
blanchet |
generate proper arity declarations for TFrees for SPASS's DFG format;
|
changeset |
files
|