wenzelm [Wed, 10 Nov 2010 15:43:06 +0100] rev 40458
treat main theory commands like headings, and nest anything else inside;
wenzelm [Wed, 10 Nov 2010 15:42:20 +0100] rev 40457
proper treatment of equal heading level;
wenzelm [Wed, 10 Nov 2010 15:41:29 +0100] rev 40456
added missing Keyword.THY_SCHEMATIC_GOAL;
more keyword categories;
wenzelm [Wed, 10 Nov 2010 15:17:25 +0100] rev 40455
default Sidekick parser based on section headings;
wenzelm [Wed, 10 Nov 2010 15:00:40 +0100] rev 40454
some support for nested source structure, based on section headings;
wenzelm [Wed, 10 Nov 2010 11:44:35 +0100] rev 40453
tuned;
wenzelm [Tue, 09 Nov 2010 23:24:46 +0100] rev 40452
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm [Tue, 09 Nov 2010 22:37:10 +0100] rev 40451
updated version;
wenzelm [Tue, 09 Nov 2010 21:52:05 +0100] rev 40450
private counter, to keep externalized ids a bit smaller;
wenzelm [Tue, 09 Nov 2010 21:44:19 +0100] rev 40449
added general Synchronized.counter convenience;
wenzelm [Tue, 09 Nov 2010 21:13:06 +0100] rev 40448
explicitly identify forked/joined tasks;
wenzelm [Tue, 09 Nov 2010 11:27:58 +0100] rev 40447
accomodate old manuals that include pdfsetup.sty without isabelle.sty;
wenzelm [Tue, 09 Nov 2010 11:17:15 +0100] rev 40446
merged
krauss [Mon, 08 Nov 2010 23:02:20 +0100] rev 40445
removed type-inference-like behaviour from relation_tac completely; tuned
wenzelm [Mon, 08 Nov 2010 20:55:27 +0100] rev 40444
avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
wenzelm [Mon, 08 Nov 2010 20:50:56 +0100] rev 40443
explicitly check uniqueness of symbol recoding;
wenzelm [Mon, 08 Nov 2010 17:44:47 +0100] rev 40442
more hints on building and running Isabelle/jEdit from command line;
wenzelm [Mon, 08 Nov 2010 14:41:11 +0100] rev 40441
merged
blanchet [Mon, 08 Nov 2010 14:33:54 +0100] rev 40440
merge
blanchet [Mon, 08 Nov 2010 14:33:30 +0100] rev 40439
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
huffman [Mon, 08 Nov 2010 05:07:18 -0800] rev 40438
merged
huffman [Sat, 06 Nov 2010 10:01:00 -0700] rev 40437
merged
huffman [Fri, 05 Nov 2010 15:15:28 -0700] rev 40436
(infixl "<<" 55) -> (infix "<<" 50)
huffman [Wed, 03 Nov 2010 17:22:25 -0700] rev 40435
simplify some proofs
huffman [Wed, 03 Nov 2010 17:06:21 -0700] rev 40434
remove unnecessary stuff from Discrete.thy
huffman [Wed, 03 Nov 2010 16:39:23 -0700] rev 40433
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
huffman [Wed, 03 Nov 2010 15:57:39 -0700] rev 40432
add lemma eq_imp_below
huffman [Wed, 03 Nov 2010 15:47:46 -0700] rev 40431
discontinue a bunch of legacy theorem names
huffman [Wed, 03 Nov 2010 15:31:24 -0700] rev 40430
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman [Wed, 03 Nov 2010 15:03:16 -0700] rev 40429
simplify some proofs
blanchet [Mon, 08 Nov 2010 13:53:18 +0100] rev 40428
compile -- 7550b2cba1cb broke the build
blanchet [Mon, 08 Nov 2010 13:25:00 +0100] rev 40427
merge