2010-05-20 haftmann 2010-05-20 moved generic List operations to theory More_List
2010-05-20 haftmann 2010-05-20 adjusted
2010-05-20 haftmann 2010-05-20 turned old-style mem into an input abbreviation
2010-05-20 wenzelm 2010-05-20 zoom font size;
2010-05-20 wenzelm 2010-05-20 added somewhat generic zoom box;
2010-05-20 wenzelm 2010-05-20 try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);
2010-05-20 wenzelm 2010-05-20 mutate displayed document synchronously in Swing thread, for improved robustness;
2010-05-20 wenzelm 2010-05-20 read style sheets only once;
2010-05-20 wenzelm 2010-05-20 handle component resize for output / HTML panel;
2010-05-20 wenzelm 2010-05-20 Isabelle_System: allow explicit isabelle_home argument;
2010-05-20 wenzelm 2010-05-20 enable shell script editor mode;
2010-05-20 wenzelm 2010-05-20 merged
2010-05-20 bulwahn 2010-05-20 merged
2010-05-20 bulwahn 2010-05-20 deactivated timing of infering modes
2010-05-19 bulwahn 2010-05-19 adapting examples
2010-05-19 bulwahn 2010-05-19 changing operations for accessing data to work with contexts
2010-05-19 bulwahn 2010-05-19 removed unnecessary Thm.transfer in the predicate compiler
2010-05-19 bulwahn 2010-05-19 changing compilation to work only with contexts; adapting quickcheck
2010-05-19 bulwahn 2010-05-19 removing unused argument in print_modes function
2010-05-19 bulwahn 2010-05-19 moving towards working with proof contexts in the predicate compiler
2010-05-19 bulwahn 2010-05-19 improved values command to handle a special case with tuples and polymorphic predicates more correctly
2010-05-19 bulwahn 2010-05-19 improved behaviour of defined_functions in the predicate compiler
2010-05-19 huffman 2010-05-19 move some example files into new HOLCF/Tutorial directory
2010-05-19 huffman 2010-05-19 remove redundant hdvd relation
2010-05-19 huffman 2010-05-19 remove unnecessary constant Fixrec.bind
2010-05-19 huffman 2010-05-19 add section about fixrec definitions with looping simp rules
2010-05-19 huffman 2010-05-19 more informative error message for fixrec when continuity proof fails
2010-05-20 wenzelm 2010-05-20 determine margin just before rendering -- proper reformatting when updating;
2010-05-20 wenzelm 2010-05-20 simplified alignment via FlowPanel; tuned;
2010-05-20 wenzelm 2010-05-20 more systematic treatment of physical document wrt. font size etc.; eliminated (crude) double buffering; tuned;
2010-05-20 wenzelm 2010-05-20 tuned;
2010-05-20 wenzelm 2010-05-20 general Isabelle_System.try_read;
2010-05-20 wenzelm 2010-05-20 explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
2010-05-20 wenzelm 2010-05-20 inverted "Freeze" to "Follow", which is the default; update unconditionally;
2010-05-19 wenzelm 2010-05-19 basic controls to freeze/update prover results;
2010-05-19 wenzelm 2010-05-19 show fully detailed protocol messages;
2010-05-19 wenzelm 2010-05-19 some updates following src/Tools/jEdit/dist-template/settings;
2010-05-19 haftmann 2010-05-19 spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
2010-05-19 haftmann 2010-05-19 merged
2010-05-19 haftmann 2010-05-19 dropped legacy_unconstrainT
2010-05-19 haftmann 2010-05-19 new version of triv_of_class machinery without legacy_unconstrain
2010-05-19 haftmann 2010-05-19 merge
2010-05-19 haftmann 2010-05-19 added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
2010-05-18 huffman 2010-05-18 remove several redundant lemmas about floor and ceiling
2010-05-18 huffman 2010-05-18 merged
2010-05-17 huffman 2010-05-17 declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-05-17 huffman 2010-05-17 simplify proof
2010-05-17 huffman 2010-05-17 simplify proof
2010-05-17 huffman 2010-05-17 remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
2010-05-18 wenzelm 2010-05-18 prefer structure Keyword and Parse;
2010-05-18 wenzelm 2010-05-18 merged
2010-05-17 huffman 2010-05-17 merged
2010-05-17 huffman 2010-05-17 remove simp attribute from square_eq_1_iff
2010-05-17 blanchet 2010-05-17 merged
2010-05-17 blanchet 2010-05-17 make sure chained facts don't pop up in the metis proof
2010-05-17 blanchet 2010-05-17 fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
2010-05-17 blanchet 2010-05-17 generate proper arity declarations for TFrees for SPASS's DFG format; and renamed a confusing function in the process
2010-05-17 blanchet 2010-05-17 identify common SPASS error more clearly
2010-05-17 huffman 2010-05-17 remove simp attribute from power2_eq_1_iff
2010-05-17 haftmann 2010-05-17 dropped old Library/Word.thy and toy example ex/Adder.thy