2010-05-10 wenzelm 2010-05-10 more convenient look-and-feel setup;
2010-05-10 wenzelm 2010-05-10 more convenient get_font;
2010-05-10 wenzelm 2010-05-10 explicit getLines(n) ensures platform-independence -- our files follow the POSIX standard, not DOS;
2010-05-10 wenzelm 2010-05-10 updated to jedit 4.3.2;
2010-05-10 wenzelm 2010-05-10 ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;
2010-05-10 wenzelm 2010-05-10 adapted to scala-2.8.0.RC2;
2010-05-10 wenzelm 2010-05-10 merged
2010-05-09 huffman 2010-05-09 real_mult_commute -> mult_commute
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-05-09 huffman 2010-05-09 remove a couple of redundant lemmas; simplify some proofs
2010-05-09 huffman 2010-05-09 merged
2010-05-08 huffman 2010-05-08 add lemmas one_less_inverse and one_le_inverse
2010-05-09 krauss 2010-05-09 do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings
2010-05-09 krauss 2010-05-09 added lemmas rel_comp_UNION_distrib(2)
2010-05-08 wenzelm 2010-05-08 made SML/NJ happy;
2010-05-09 wenzelm 2010-05-09 reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
2010-05-09 wenzelm 2010-05-09 Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
2010-05-09 wenzelm 2010-05-09 just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
2010-05-09 wenzelm 2010-05-09 added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
2010-05-09 wenzelm 2010-05-09 tuned;
2010-05-09 wenzelm 2010-05-09 removed unused "option" variants of "same" operations;
2010-05-09 wenzelm 2010-05-09 more basic replacement of newlines;
2010-05-09 wenzelm 2010-05-09 static Symbol.spaces;
2010-05-08 wenzelm 2010-05-08 proper use of var stopped;
2010-05-08 wenzelm 2010-05-08 removed junk;
2010-05-08 wenzelm 2010-05-08 tuned headers;
2010-05-08 wenzelm 2010-05-08 tuned;
2010-05-08 wenzelm 2010-05-08 merged
2010-05-08 haftmann 2010-05-08 merged
2010-05-08 haftmann 2010-05-08 moved normalization proof tool infrastructure to canonical algebraic classes
2010-05-08 nipkow 2010-05-08 added lemmas
2010-05-08 haftmann 2010-05-08 merged
2010-05-07 haftmann 2010-05-07 renamed Normalizer to the more specific Semiring_Normalizer
2010-05-07 haftmann 2010-05-07 delete Groebner_Basis directory -- only one file left
2010-05-07 haftmann 2010-05-07 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
2010-05-07 haftmann 2010-05-07 merged
2010-05-07 haftmann 2010-05-07 moved lemma zdvd_period to theory Int
2010-05-08 wenzelm 2010-05-08 tuned;
2010-05-08 wenzelm 2010-05-08 discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
2010-05-08 wenzelm 2010-05-08 tuned error message: regular Pretty.string_of instead of raw Pretty.output;
2010-05-08 wenzelm 2010-05-08 unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;
2010-05-08 wenzelm 2010-05-08 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-05-08 wenzelm 2010-05-08 prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";
2010-05-08 wenzelm 2010-05-08 tuned signature;
2010-05-08 wenzelm 2010-05-08 added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
2010-05-08 wenzelm 2010-05-08 back-patching of axclass proofs;
2010-05-08 wenzelm 2010-05-08 back-patching via Single_Assignment.var;
2010-05-07 wenzelm 2010-05-07 support several sidekick parsers -- very basic default parser;
2010-05-07 wenzelm 2010-05-07 sidekick: unformatted content, notably without newlines;
2010-05-07 wenzelm 2010-05-07 unformatted output;
2010-05-07 wenzelm 2010-05-07 output symbolic pretty printing markup and format in the front end;
2010-05-07 wenzelm 2010-05-07 Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version; tuned;
2010-05-07 wenzelm 2010-05-07 tuned;
2010-05-07 wenzelm 2010-05-07 strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
2010-05-07 wenzelm 2010-05-07 use existing undefined function;
2010-05-07 wenzelm 2010-05-07 merged
2010-05-07 krauss 2010-05-07 removed semicolons
2010-05-07 krauss 2010-05-07 rule subrelI (for nice Isar proofs of relation inequalities)
2010-05-07 wenzelm 2010-05-07 merged