merged

added missing dependencies; simplified (by overapproximating a bit); alphabetical order

merged

merged

tuned notation and proofs

move error logic closer to user

allow lambda-lifting without triggers

move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)

added option to control which lambda translation to use (for experiments)

fix subtle type inference bug in Metis -- different occurrences of the same Skolem might need to be typed differently, using paramify_vars overconstraints the typing problem

use monomorphic encoding as fallback, since they tend to produce fewer type errors

don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes

clearer unsound message

clarify fine soundness point

always unfold "Let"s is Sledgehammer, Metis, and MESON

unbreak Nitrox's parsing

merged

tuned lemma positions and proofs

tuned notation

uniqueness lemmas for bot and top

adjusted to tightened specification of classes bot and top

moved lemmas bot_less and less_top to classes bot and top respectively

tightened specification of classes bot and top: uniqueness of top and bot elements

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

better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6

more exhaustive testing in Nitrox

no timeout for Nitrox

avoid relying on piping to "isabelle tty", because this gives errors on some Linuxes about the standard input not being a tty

added arithmetic decision procedure to CASC setup

added some arithmetic functions, for THF with arithmetic

pull in arithmetic theories

cleanly separate TPTP related files from other examples

increasing timeout to avoid spurious failures

merged

more generalization towards complete lattices

experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package

merge

Tuned

more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;

added term_sharing.ML;

recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;

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;

low-level tuning;

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;

XML.pretty with depth limit;

more thorough Variable.check_name: Binding.check for logical entities within the term language;

tuned;

merged

Update HOLLightCompat

Update files generated in HOL/Import/HOLLight

HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems

ML pp for XML.tree;

made SML/NJ happy;

clarified YXML.detect;

retain some terminology of "XML attributes";

more uniform Properties in ML and Scala;

more uniform Term and Term_XML modules;

more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;

tuned signature -- less cryptic ASCII names;

discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;

added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;

added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;

more precise Symbol_Pos.quote_string;

clarified YXML.embed_controls -- this is idempotent and cannot be nested;

allow empty body for raw_message -- important for Invoke_Scala;

Isabelle string syntax allows literal control characters;

glyphs from DejaVu for ASCII control characters 5, 6, 7, 127, which have a special meaning in Isabelle or Poly/ML;

more precise exceptions;

tuned XML modules;

Quotient example: Lists with distinct elements

merged

explicit code equation for equality

tuned error messages;

tuned;

tuned signature -- corresponding to Scala version;

made SML/NJ happy; tuned error;

more uniform padded_markup, which is important for caret visibility despite absence of markup;

merged

merged

tuned proofs

tuned notation

tuned notation

tuned notation

NEWS;

proper InvocationTargetException.getCause for indirect exceptions; capture hard errors to ensure protocol integrity; tuned error messages;

tuned error message;

tuned signature;

JVM method invocation service via Scala layer;

tuned signature;

some support for raw messages, which bypass standard Symbol/YXML decoding; tuned signature;

tuned XML.Cache parameters;

some support to invoke Scala methods under program control;

merged;

merged

tuned proofs and notation

more succinct proofs

more succinct proofs

adding a very liberal timeout for values after a test case failed due to the restricted timeout

improved NEWS

NEWS

standardized String.concat towards implode (cf. c37a1f29bbc0)

adding quickcheck examples for evaluating floor and ceiling functions

adding code equations to execute floor and ceiling on rational and real numbers

adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)

inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature;

lambda terms with XML data representation in Scala; avoid `class` in signature;

XML data representation of lambda terms;

YXML.string_of_body convenience;

made SML/NJ happy;

tuned signature;

more abstract signature; tuned;

simplified XML_Data;

less currying in Scala;

propagate header changes to prover process; simplified Document case classes; Document.State.assignments: indexed by Version_ID;

echo prover input via raw_messages, for improved protocol tracing;

tuned;

tuned signature;

clarified propagation of node name and header;

more precise treatment of prover definedness;

tuned source structure;