2010-11-11 wenzelm 2010-11-11 unified type Document.Edit;
2010-11-11 wenzelm 2010-11-11 replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes; Document_Model.pending_edits: more robust treatment of init, including buffer reload event (jEdit 4.3.2 produces malformed remove/insert that lacks the last character); tuned;
2010-11-11 wenzelm 2010-11-11 tuned;
2010-11-11 wenzelm 2010-11-11 reduced danger of line breaks within minipage;
2010-11-10 wenzelm 2010-11-10 Sidekick block asset: show first line only;
2010-11-10 wenzelm 2010-11-10 added buffer_text convenience, with explicit locking;
2010-11-10 wenzelm 2010-11-10 use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading);
2010-11-10 wenzelm 2010-11-10 merged
2010-11-10 blanchet 2010-11-10 make SML/NJ happy
2010-11-09 haftmann 2010-11-09 merged
2010-11-09 haftmann 2010-11-09 slightly changed fun_map_def
2010-11-09 haftmann 2010-11-09 fun_rel_def is no simp rule by default
2010-11-09 haftmann 2010-11-09 more appropriate specification packages; fun_rel_def is no simp rule by default
2010-11-09 haftmann 2010-11-09 type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
2010-11-09 haftmann 2010-11-09 more appropriate specification packages; fun_rel_def is no simp rule by default
2010-11-09 haftmann 2010-11-09 type annotations in specifications; fun_rel_def is no simp rule by default
2010-11-09 haftmann 2010-11-09 fun_rel_def is no simp rule by default
2010-11-09 paulson 2010-11-09 merged
2010-11-09 paulson 2010-11-09 tidied using metis
2010-11-10 wenzelm 2010-11-10 manage folding via sidekick by default;
2010-11-10 wenzelm 2010-11-10 eliminated obsolete heading category -- superseded by heading_level;
2010-11-10 wenzelm 2010-11-10 treat main theory commands like headings, and nest anything else inside;
2010-11-10 wenzelm 2010-11-10 proper treatment of equal heading level;
2010-11-10 wenzelm 2010-11-10 added missing Keyword.THY_SCHEMATIC_GOAL; more keyword categories;
2010-11-10 wenzelm 2010-11-10 default Sidekick parser based on section headings;
2010-11-10 wenzelm 2010-11-10 some support for nested source structure, based on section headings;
2010-11-10 wenzelm 2010-11-10 tuned;
2010-11-09 wenzelm 2010-11-09 misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
2010-11-09 wenzelm 2010-11-09 updated version;
2010-11-09 wenzelm 2010-11-09 private counter, to keep externalized ids a bit smaller;
2010-11-09 wenzelm 2010-11-09 added general Synchronized.counter convenience;
2010-11-09 wenzelm 2010-11-09 explicitly identify forked/joined tasks;
2010-11-09 wenzelm 2010-11-09 accomodate old manuals that include pdfsetup.sty without isabelle.sty;
2010-11-09 wenzelm 2010-11-09 merged
2010-11-08 krauss 2010-11-08 removed type-inference-like behaviour from relation_tac completely; tuned
2010-11-08 wenzelm 2010-11-08 avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
2010-11-08 wenzelm 2010-11-08 explicitly check uniqueness of symbol recoding;
2010-11-08 wenzelm 2010-11-08 more hints on building and running Isabelle/jEdit from command line;
2010-11-08 wenzelm 2010-11-08 merged
2010-11-08 blanchet 2010-11-08 merge
2010-11-08 blanchet 2010-11-08 reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
2010-11-08 huffman 2010-11-08 merged
2010-11-06 huffman 2010-11-06 merged
2010-11-05 huffman 2010-11-05 (infixl "<<" 55) -> (infix "<<" 50)
2010-11-03 huffman 2010-11-03 simplify some proofs
2010-11-03 huffman 2010-11-03 remove unnecessary stuff from Discrete.thy
2010-11-03 huffman 2010-11-03 remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
2010-11-03 huffman 2010-11-03 add lemma eq_imp_below
2010-11-03 huffman 2010-11-03 discontinue a bunch of legacy theorem names
2010-11-03 huffman 2010-11-03 move a few admissibility lemmas into FOCUS/Stream_adm.thy
2010-11-03 huffman 2010-11-03 simplify some proofs
2010-11-08 blanchet 2010-11-08 compile -- 7550b2cba1cb broke the build
2010-11-08 blanchet 2010-11-08 merge
2010-11-08 blanchet 2010-11-08 recognize Vampire error
2010-11-08 boehmes 2010-11-08 return the process return code along with the process outputs
2010-11-08 boehmes 2010-11-08 better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-11-08 haftmann 2010-11-08 merged
2010-11-08 haftmann 2010-11-08 corrected slip: must keep constant map, not type map; tuned code
2010-11-08 haftmann 2010-11-08 constructors to datatypes in code_reflect can be globbed; dropped unused code
2010-11-08 bulwahn 2010-11-08 adding code and theory for smallvalue generators, but do not setup the interpretation yet