Respectfullness and preservation of list_rel

replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo; simplified via ProofContext.check_tfree;

get_sort: suppress dummyS from input; added check_tvar, check_tfree convenience; tuned;

modernized treatment of sort constraints in specification; pass-through type variables as usual as (string * sort) internally -- recovers proper sort handling;

typecopy: observe given sort constraints more precisely;

inline old Record.read_typ/cert_typ; spelling;

spelling;

theory RBT with abstract type of red-black trees backed by implementation RBT_Impl

tuned whitespace;

merged

merged

added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture

make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second

make Sledgehammer's "timeout" option work for "minimize"

fixed handling of "sledgehammer_params" that get a default value from Isabelle menu; and added "atp" as alias for "atps"

Spelling error: theroems -> theorems

advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.

record package: corrected sort handling in type translations to avoid crashes when default sort is changed. Test case: record 'a T = elem :: 'a defaultsort order term elem (* low-level exception *)

more precise treatment of UNC server prefix, e.g. //foo;

support named_root, which approximates UNC server prefix (for Cygwin); tuned representation: reversed elements; misc simplification and cleanup;

updated Thm.add_axiom/add_def;

adapted PUBLISH_TEST for atbroy102, which only mounts /home/isatest;

bring HOLCF/ex/Domain_Proofs.thy up to date

adapt Refute example to reflect latest soundness fix to Refute

commented out unsound "lfp"/"gfp" handling + fixed set output syntax; the "lfp"/"gfp" bug can be reproduced by looking for a counterexample to lemma "(A \<union> B)^+ = A^+ \<union> B^+" Refute incorrectly finds a countermodel for cardinality 1 (the smallest counterexample requires cardinality 2).

merged

make Nitpick output everything to tracing in debug mode; so that when an exception occurs, I can switch to the tracing window to see what was in the response window before the exception blew everything away

fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")

cosmetics

merge