2011-06-29 wenzelm 2011-06-29 tuned signature;
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2011-06-29 wenzelm 2011-06-29 print Path.T with some markup;
2011-06-29 wenzelm 2011-06-29 HTML: render control symbols more like Isabelle/Scala/jEdit;
2011-06-28 traytel 2011-06-28 collapse map functions with identity subcoercions to identities;
2011-06-28 blanchet 2011-06-28 reenabled accidentally-disabled automatic minimization
2011-06-28 wenzelm 2011-06-28 tuned markup;
2011-06-28 paulson 2011-06-28 merged
2011-06-28 paulson 2011-06-28 tidied messy proofs
2011-06-28 bulwahn 2011-06-28 merged
2011-06-28 bulwahn 2011-06-28 adding timeout to quickcheck narrowing
2011-06-28 paulson 2011-06-28 simplified proofs using metis calls
2011-06-28 paulson 2011-06-28 merged
2011-06-28 paulson 2011-06-28 keyfree: The set of key-free messages (and associated theorems)
2011-06-27 wenzelm 2011-06-27 merged
2011-06-27 krauss 2011-06-27 new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor; renamed old version to info_of_constr_permissive, reflecting its semantics
2011-06-27 blanchet 2011-06-27 added reference for MESON
2011-06-27 blanchet 2011-06-27 document "meson" and "metis" in HOL specific section of the Isar ref manual
2011-06-27 blanchet 2011-06-27 clarify minimizer output
2011-06-27 blanchet 2011-06-27 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
2011-06-27 blanchet 2011-06-27 tweaked comment
2011-06-27 blanchet 2011-06-27 document "sound" option
2011-06-27 blanchet 2011-06-27 minor Sledgehammer news
2011-06-27 blanchet 2011-06-27 added "sound" option to force Sledgehammer to be pedantically sound
2011-06-27 blanchet 2011-06-27 removed "full_types" option from documentation
2011-06-27 blanchet 2011-06-27 document changes to Sledgehammer and "try"
2011-06-27 blanchet 2011-06-27 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
2011-06-27 blanchet 2011-06-27 clarify warning message to avoid confusing beginners
2011-06-27 blanchet 2011-06-27 remove experimental trimming feature -- it slowed down things on Linux for some reason
2011-06-27 blanchet 2011-06-27 filter out some tautologies using an ATP, especially for those theories that are known for producing such things
2011-06-27 wenzelm 2011-06-27 NEWS;
2011-06-27 wenzelm 2011-06-27 document antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27 wenzelm 2011-06-27 proper checking of @{ML_antiquotation};
2011-06-27 wenzelm 2011-06-27 hide rather short auxiliary names, which can easily occur in user theories;
2011-06-27 wenzelm 2011-06-27 updated generated file;
2011-06-27 wenzelm 2011-06-27 ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;
2011-06-27 wenzelm 2011-06-27 old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
2011-06-27 wenzelm 2011-06-27 parallel Syntax.parse, which is rather slow;
2011-06-27 wenzelm 2011-06-27 markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";
2011-06-27 hoelzl 2011-06-27 move conditional expectation to its own theory file
2011-06-26 boehmes 2011-06-26 updated SMT certificates
2011-06-26 boehmes 2011-06-26 generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem); maintain extra-logical information when introducing explicit application; handle let-expressions properly
2011-06-25 wenzelm 2011-06-25 proper tokens only if session is ready;
2011-06-25 wenzelm 2011-06-25 entity markup for "type", "constant";
2011-06-25 wenzelm 2011-06-25 clarified Markup.CLASS vs. HTML.CLASS;
2011-06-25 wenzelm 2011-06-25 tuned color, to avoid confusion with type variables;
2011-06-25 wenzelm 2011-06-25 discontinued generic XML markup -- this is for XHTML with <span/> elements;
2011-06-25 wenzelm 2011-06-25 type classes: entity markup instead of old-style token markup;
2011-06-25 wenzelm 2011-06-25 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
2011-06-25 wenzelm 2011-06-25 clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example; discontinued unused Binding.qualified_name_of;
2011-06-25 wenzelm 2011-06-25 produce string constant directly;
2011-06-25 wenzelm 2011-06-25 merged
2011-06-25 ballarin 2011-06-25 While reading equations of an interpretation, already allow syntax provided by the interpretation base.
2011-06-25 wenzelm 2011-06-25 removed very slow proof of unnamed/unused theorem from HOL/Quickcheck_Narrowing.thy (cf. 2dee03f192b7) -- can take seconds for main HOL and minutes for HOL-Proofs;
2011-06-25 wenzelm 2011-06-25 clarified java.ext.dirs: putting Isabelle extensions first makes it work miraculously even on Cygwin with Java in "C:\Program Files\..." (with spaces in file name);
2011-06-25 wenzelm 2011-06-25 CLASSPATH already converted in isabelle java wrapper;
2011-06-25 wenzelm 2011-06-25 removed unused/broken Isabelle.exe for now -- needs update of Admin/launch4j;
2011-06-23 wenzelm 2011-06-23 more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!