2010-01-10 berghofe 2010-01-10 Adapted to changes in setup of induct method.
2010-01-10 berghofe 2010-01-10 Expand proofs of induct_atomize'/rulify'.
2010-01-10 berghofe 2010-01-10 Changed case names of converse_rtranclp_induct.
2010-01-10 berghofe 2010-01-10 Injectivity / distinctness theorems are now used to simplify induction rules.
2010-01-10 berghofe 2010-01-10 same_append_eq / append_same_eq are now used for simplifying induction rules.
2010-01-10 berghofe 2010-01-10 Tuned some proofs; nicer case names for some of the induction / cases rules.
2010-01-10 berghofe 2010-01-10 Added setup for simplification of equality constraints in induction rules.
2010-01-10 berghofe 2010-01-10 Added infrastructure for simplifying equality constraints. Option (no_simp) restores old behaviour of induct method.
2010-01-15 haftmann 2010-01-15 spurious proof failure
2010-01-14 haftmann 2010-01-14 merged
2010-01-14 haftmann 2010-01-14 merged
2010-01-14 haftmann 2010-01-14 dropped unused binding
2010-01-14 haftmann 2010-01-14 dedicated conversions to and from Int
2010-01-14 haftmann 2010-01-14 printing of cases
2010-01-14 haftmann 2010-01-14 tuned for products vs. tupled functions
2010-01-14 haftmann 2010-01-14 added Scala setup
2010-01-14 haftmann 2010-01-14 allow individual printing of numerals during code serialization
2010-01-14 blanchet 2010-01-14 reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
2010-01-14 haftmann 2010-01-14 adjusted to changes in code equation administration
2010-01-13 haftmann 2010-01-13 explicit abstract type of code certificates
2010-01-13 haftmann 2010-01-13 corrected error messages; tuned
2010-01-13 haftmann 2010-01-13 function transformer preprocessor applies to both code generators
2010-01-13 haftmann 2010-01-13 merged
2010-01-12 haftmann 2010-01-12 code certificates as integral part of code generation
2010-01-13 haftmann 2010-01-13 import of antiquote_setup not necessary
2010-01-13 haftmann 2010-01-13 merged
2010-01-13 haftmann 2010-01-13 being more accurate wrt. list syntax
2010-01-13 haftmann 2010-01-13 deactivate pretty code test for Scala -- no proper setup yet
2010-01-13 haftmann 2010-01-13 some syntax setup for Scala
2010-01-13 wenzelm 2010-01-13 added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
2010-01-12 wenzelm 2010-01-12 merged
2010-01-12 paulson 2010-01-12 Parsing errors during proof reconstruction now give rise to an intelligible error message.
2010-01-12 wenzelm 2010-01-12 rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs; misc cleanup of mathematical glyphs, with bold version synthesized by fontforge;
2010-01-12 wenzelm 2010-01-12 tuned initial properties/perspective;
2010-01-12 wenzelm 2010-01-12 provide JEDIT_SETTINGS via settings; provide default perspective; tuned default properties;
2010-01-12 wenzelm 2010-01-12 updated version and dependencies;
2010-01-12 wenzelm 2010-01-12 recovered subscript (cf. ded5b770ec1c);
2010-01-12 haftmann 2010-01-12 formal antiquotations for ML snippets; no "open" unsynchronized references
2010-01-11 wenzelm 2010-01-11 clarified terminology;
2010-01-11 wenzelm 2010-01-11 merged
2010-01-11 haftmann 2010-01-11 added code certificates
2010-01-11 haftmann 2010-01-11 tuned code equations
2010-01-11 hoelzl 2010-01-11 Matrices form a semiring with 0
2010-01-11 wenzelm 2010-01-11 incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
2010-01-11 wenzelm 2010-01-11 ignore some src/Tools/jEdit stuff;
2010-01-11 wenzelm 2010-01-11 merged with converted/relocated copy of http://isabelle.in.tum.de/repos/isabelle-jedit/rev/93d884afa74b
2010-01-11 wenzelm 2010-01-11 more timing;
2010-01-11 wenzelm 2010-01-11 more tobust treatment of Document.current_state; some timing;
2010-01-11 wenzelm 2010-01-11 new unparsed span for text right after existing command; tuned;
2010-01-11 wenzelm 2010-01-11 Outer_Lex.is_ignored;
2010-01-11 wenzelm 2010-01-11 simplified Text_Edit;
2010-01-11 wenzelm 2010-01-11 eliminated strange mutable var commands; removed_commands: refer to old commands; misc tuning;
2010-01-11 wenzelm 2010-01-11 updated header;
2010-01-11 wenzelm 2010-01-11 eliminated obsolete isabelle.proofdocument.Token;
2010-01-11 wenzelm 2010-01-11 do not override Command.hashCode -- which was inconsistent with eq anyway; unparsed: no id, commands observe pointer equality; actually invoke edit_commands; more correct doc_edits; tuned;
2010-01-11 wenzelm 2010-01-11 renamed Command.content to source; reorganization of document parsing, using command spans etc. -- initial setup;
2010-01-10 wenzelm 2010-01-10 further tuning of command_start;
2010-01-10 wenzelm 2010-01-10 refrain from poking blink rate -- might get stuck in invisible state;
2010-01-10 wenzelm 2010-01-10 eliminated Command.stop, which tends to case duplicate traversal of commands;
2010-01-10 wenzelm 2010-01-10 iterators for ranges of commands/starts -- avoid extra array per document; try/finally for saved_color; misc tuning;