2010-04-15 blanchet 2010-04-15 make Sledgehammer's output more debugging friendly
2010-04-16 wenzelm 2010-04-16 made SML/NJ happy;
2010-04-16 wenzelm 2010-04-16 proper masking of dummy name_space;
2010-04-16 wenzelm 2010-04-16 salvaged some ML functors from decay, which is the natural consequence of lack of formal checking;
2010-04-16 wenzelm 2010-04-16 proper checking of ML functors (in Poly/ML 5.2 or later); eliminated pathetic comments;
2010-04-16 wenzelm 2010-04-16 added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
2010-04-16 wenzelm 2010-04-16 isatest: improved treatment of local files on atbroy102;
2010-04-15 huffman 2010-04-15 add rule deflation_ID to proof script for take + constructor rules
2010-04-15 wenzelm 2010-04-15 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);
2010-04-15 wenzelm 2010-04-15 HOL record: explicitly allow sort constraints;
2010-04-15 wenzelm 2010-04-15 misc tuning and simplification;
2010-04-15 wenzelm 2010-04-15 explicit ProofContext.check_tfree;
2010-04-15 wenzelm 2010-04-15 merged
2010-04-15 Cezary Kaliszyk 2010-04-15 Respectfullness and preservation of list_rel
2010-04-15 wenzelm 2010-04-15 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;
2010-04-15 wenzelm 2010-04-15 get_sort: suppress dummyS from input; added check_tvar, check_tfree convenience; tuned;
2010-04-15 wenzelm 2010-04-15 modernized treatment of sort constraints in specification; pass-through type variables as usual as (string * sort) internally -- recovers proper sort handling;
2010-04-15 wenzelm 2010-04-15 typecopy: observe given sort constraints more precisely;
2010-04-15 wenzelm 2010-04-15 inline old Record.read_typ/cert_typ; spelling;
2010-04-15 wenzelm 2010-04-15 spelling;
2010-04-15 haftmann 2010-04-15 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
2010-04-14 wenzelm 2010-04-14 tuned whitespace;
2010-04-14 wenzelm 2010-04-14 merged
2010-04-14 blanchet 2010-04-14 merged
2010-04-14 blanchet 2010-04-14 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
2010-04-14 blanchet 2010-04-14 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
2010-04-14 blanchet 2010-04-14 make Sledgehammer's "timeout" option work for "minimize"
2010-04-14 blanchet 2010-04-14 fixed handling of "sledgehammer_params" that get a default value from Isabelle menu; and added "atp" as alias for "atps"
2010-04-14 hoelzl 2010-04-14 Spelling error: theroems -> theorems
2010-04-14 krauss 2010-04-14 advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
2010-04-14 krauss 2010-04-14 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 *)
2010-04-14 wenzelm 2010-04-14 more precise treatment of UNC server prefix, e.g. //foo;
2010-04-14 wenzelm 2010-04-14 support named_root, which approximates UNC server prefix (for Cygwin); tuned representation: reversed elements; misc simplification and cleanup;
2010-04-14 wenzelm 2010-04-14 updated Thm.add_axiom/add_def;
2010-04-14 wenzelm 2010-04-14 adapted PUBLISH_TEST for atbroy102, which only mounts /home/isatest;
2010-04-13 huffman 2010-04-13 bring HOLCF/ex/Domain_Proofs.thy up to date
2010-04-13 blanchet 2010-04-13 adapt Refute example to reflect latest soundness fix to Refute
2010-04-13 blanchet 2010-04-13 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).
2010-04-13 blanchet 2010-04-13 merged
2010-04-13 blanchet 2010-04-13 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
2010-04-13 blanchet 2010-04-13 fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
2010-04-13 blanchet 2010-04-13 cosmetics
2010-04-13 Cezary Kaliszyk 2010-04-13 merge
2010-04-13 Cezary Kaliszyk 2010-04-13 merge
2010-04-13 Cezary Kaliszyk 2010-04-13 add If respectfullness and preservation to Quotient package database
2010-04-13 haftmann 2010-04-13 more accurate pattern match
2010-04-13 haftmann 2010-04-13 dropped dead code
2010-04-12 huffman 2010-04-12 update domain package examples
2010-04-12 huffman 2010-04-12 remove dead code
2010-04-12 huffman 2010-04-12 share more code between definitional and axiomatic domain packages
2010-04-12 huffman 2010-04-12 for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
2010-04-12 Cezary Kaliszyk 2010-04-12 Changed the type of Quot_True, so that it is an HOL constant.
2010-04-11 haftmann 2010-04-11 removed rather toyish tree
2010-04-11 haftmann 2010-04-11 updated keywords
2010-04-11 haftmann 2010-04-11 merged
2010-04-11 haftmann 2010-04-11 user interface for abstract datatypes is an attribute, not a command
2010-04-11 haftmann 2010-04-11 implementation of mappings by rbts
2010-04-11 haftmann 2010-04-11 lemma is_empty_empty
2010-04-11 haftmann 2010-04-11 constructor Mapping replaces AList
2010-04-11 wenzelm 2010-04-11 stay within Local_Defs layer;