system properties determine the JVM platform, not the Isabelle one;

THIS_CYGWIN;

improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;

isatest: more robust treatment of remote files, less reliance on mounted file system;

merged

added missing \n in output

by default, don't try to start ATPs that aren't installed

fiddle with Sledgehammer option syntax

added timestamp to proof

restore order of clauses in TPTP output; there's a rather subtle invariant w.r.t. "extract_lemmas"

optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time; saves 2 sec per Sledgehammer invocation on my laptop!

output total time taken by Sledgehammer if "verbose" is set

Sledgehammer: the empty set of fact () should mean nothing, not unchanged

reorganize Sledgehammer's relevance filter slightly

tell the user that Sledgehammer kills its siblings

updated keywords;

replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix); misc tuning and simplification;

keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;

separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

allow syntax types within abbreviations;

modernized old-style type abbreviations;

modernized type abbreviations;

local type abbreviations;

merged

added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)

store nonmangled names along with mangled type names in Sledgehammer for debugging purposes

give more sensible names to "fol_type" constructors, as requested by a FIXME comment

make Sledgehammer's output more debugging friendly

made SML/NJ happy;

proper masking of dummy name_space;

salvaged some ML functors from decay, which is the natural consequence of lack of formal checking;

proper checking of ML functors (in Poly/ML 5.2 or later); eliminated pathetic comments;

added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;

isatest: improved treatment of local files on atbroy102;

add rule deflation_ID to proof script for take + constructor rules

more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);

HOL record: explicitly allow sort constraints;

misc tuning and simplification;

explicit ProofContext.check_tfree;

merged

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

merge

add If respectfullness and preservation to Quotient package database

more accurate pattern match

dropped dead code

update domain package examples

remove dead code

share more code between definitional and axiomatic domain packages

for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML

Changed the type of Quot_True, so that it is an HOL constant.

removed rather toyish tree

updated keywords

merged

user interface for abstract datatypes is an attribute, not a command

implementation of mappings by rbts

lemma is_empty_empty

constructor Mapping replaces AList

stay within Local_Defs layer;

expose foundational typedef axiom name;

Thm.add_axiom/add_def: return internal name of foundational axiom;

modernized datatype constructors;

of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;

tuned;

of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;

include JEDIT_APPLE_PROPERTIES by default;

isatest: more uniform setup for Unix vs. Cygwin;