2011-07-13 haftmann 2011-07-13 adjusted to tightened specification of classes bot and top
2011-07-13 haftmann 2011-07-13 moved lemmas bot_less and less_top to classes bot and top respectively
2011-07-13 haftmann 2011-07-13 tightened specification of classes bot and top: uniqueness of top and bot elements
2011-07-13 blanchet 2011-07-13 honor the TPTP environment variable as the root of include relative paths -- that's a weird convention but without it Nitrox will fail at CASC
2011-07-13 blanchet 2011-07-13 better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6
2011-07-13 blanchet 2011-07-13 more exhaustive testing in Nitrox
2011-07-13 blanchet 2011-07-13 no timeout for Nitrox
2011-07-13 blanchet 2011-07-13 avoid relying on piping to "isabelle tty", because this gives errors on some Linuxes about the standard input not being a tty
2011-07-13 blanchet 2011-07-13 added arithmetic decision procedure to CASC setup
2011-07-13 blanchet 2011-07-13 added some arithmetic functions, for THF with arithmetic
2011-07-13 blanchet 2011-07-13 pull in arithmetic theories
2011-07-13 blanchet 2011-07-13 cleanly separate TPTP related files from other examples
2011-07-13 bulwahn 2011-07-13 increasing timeout to avoid spurious failures
2011-07-13 haftmann 2011-07-13 merged
2011-07-13 haftmann 2011-07-13 more generalization towards complete lattices
2011-07-13 krauss 2011-07-13 experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
2011-07-13 Cezary Kaliszyk 2011-07-13 merge
2011-07-13 Cezary Kaliszyk 2011-07-13 Tuned
2011-07-14 wenzelm 2011-07-14 more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
2011-07-13 wenzelm 2011-07-13 added term_sharing.ML;
2011-07-13 wenzelm 2011-07-13 recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
2011-07-13 wenzelm 2011-07-13 sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML); minor tuning;
2011-07-13 wenzelm 2011-07-13 low-level tuning;
2011-07-13 wenzelm 2011-07-13 Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one; Sorts.certify_class: prefer the persistent name;
2011-07-13 wenzelm 2011-07-13 XML.pretty with depth limit;
2011-07-12 wenzelm 2011-07-12 more thorough Variable.check_name: Binding.check for logical entities within the term language;
2011-07-12 wenzelm 2011-07-12 tuned;
2011-07-12 wenzelm 2011-07-12 merged
2011-07-13 Cezary Kaliszyk 2011-07-13 Update HOLLightCompat
2011-07-13 Cezary Kaliszyk 2011-07-13 Update files generated in HOL/Import/HOLLight
2011-07-13 Cezary Kaliszyk 2011-07-13 HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems
2011-07-12 wenzelm 2011-07-12 ML pp for XML.tree;
2011-07-12 wenzelm 2011-07-12 made SML/NJ happy;
2011-07-12 wenzelm 2011-07-12 clarified YXML.detect;
2011-07-12 wenzelm 2011-07-12 retain some terminology of "XML attributes";
2011-07-12 wenzelm 2011-07-12 more uniform Properties in ML and Scala;
2011-07-12 wenzelm 2011-07-12 more uniform Term and Term_XML modules;
2011-07-12 wenzelm 2011-07-12 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
2011-07-12 wenzelm 2011-07-12 tuned signature -- less cryptic ASCII names;
2011-07-12 wenzelm 2011-07-12 discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;
2011-07-12 wenzelm 2011-07-12 added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
2011-07-12 wenzelm 2011-07-12 added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
2011-07-12 wenzelm 2011-07-12 more precise Symbol_Pos.quote_string;
2011-07-12 wenzelm 2011-07-12 clarified YXML.embed_controls -- this is idempotent and cannot be nested;
2011-07-12 wenzelm 2011-07-12 allow empty body for raw_message -- important for Invoke_Scala;
2011-07-12 wenzelm 2011-07-12 Isabelle string syntax allows literal control characters;
2011-07-12 wenzelm 2011-07-12 glyphs from DejaVu for ASCII control characters 5, 6, 7, 127, which have a special meaning in Isabelle or Poly/ML;
2011-07-12 wenzelm 2011-07-12 more precise exceptions;
2011-07-12 wenzelm 2011-07-12 tuned XML modules;
2011-07-12 Cezary Kaliszyk 2011-07-12 Quotient example: Lists with distinct elements
2011-07-11 wenzelm 2011-07-11 merged
2011-07-11 haftmann 2011-07-11 explicit code equation for equality
2011-07-11 wenzelm 2011-07-11 tuned error messages;
2011-07-11 wenzelm 2011-07-11 tuned;
2011-07-11 wenzelm 2011-07-11 tuned signature -- corresponding to Scala version;
2011-07-11 wenzelm 2011-07-11 made SML/NJ happy; tuned error;
2011-07-11 wenzelm 2011-07-11 more uniform padded_markup, which is important for caret visibility despite absence of markup;
2011-07-11 wenzelm 2011-07-11 merged
2011-07-11 haftmann 2011-07-11 merged
2011-07-10 haftmann 2011-07-10 tuned proofs