2011-03-28 wenzelm 2011-03-28 address serious problem of type inference (introduced in 6f085332c7d3): _type_constraint_ needs type scheme A --> A with proper scope of parameters, otherwise term "(f :: _ => _) :: 'c => 'c" will get type "'a => 'b", for example;
2011-03-28 krauss 2011-03-28 raised various timeouts to accommodate sluggish SML/NJ
2011-03-28 bulwahn 2011-03-28 changing values_timeout from a static option to a dynamic option as required for testing with SML/NJ
2011-03-28 krauss 2011-03-28 keep smlnj HOL images around
2011-03-27 wenzelm 2011-03-27 merged
2011-03-27 krauss 2011-03-27 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj"; adapted test configuration SML_makeall
2011-03-27 krauss 2011-03-27 avoid *** in normal output, which usually marks errors in logs
2011-03-27 wenzelm 2011-03-27 added Markup.Name and Markup.Kind convenience; token_style for entity kind markup;
2011-03-27 wenzelm 2011-03-27 decode_term: some context-sensitive markup; more informative Markup.entity and Name_Space.markup_entry; Markup.const: use "constant" to make it coincide with name space kind;
2011-03-27 wenzelm 2011-03-27 tuned signatures;
2011-03-27 wenzelm 2011-03-27 decode_term: more precise reports;
2011-03-27 wenzelm 2011-03-27 adhoc token style for free/bound;
2011-03-27 wenzelm 2011-03-27 decode_term/disambig: report resolved term variables for the unique (!) result;
2011-03-27 wenzelm 2011-03-27 removed unclear comments stemming from ed24ba6f69aa;
2011-03-26 wenzelm 2011-03-26 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
2011-03-26 wenzelm 2011-03-26 added Future.cond_forks convenience;
2011-03-26 wenzelm 2011-03-26 Isabelle_System.create_tmp_path/with_tmp_file: optional extension; thread-safe versions of Present.display_graph, Present.isabelle_browser, Present.drafts -- using Isabelle_System.with_tmp_dir;
2011-03-26 wenzelm 2011-03-26 tuned;
2011-03-26 wenzelm 2011-03-26 more direct loose_bvar1; tuned; slight re-unification of clone (cf. 47f8bfe0f597);
2011-03-26 wenzelm 2011-03-26 suppress Mercurial backup files; uniform treatment of tool filtering in bash/perl/scala;
2011-03-26 wenzelm 2011-03-26 updated generated file; tuned whitespace;
2011-03-26 wenzelm 2011-03-26 merged
2011-03-26 krauss 2011-03-26 SML_makeall: run with -j 3
2011-03-25 krauss 2011-03-25 fixed incomplete rename (1cdf54e845fa)
2011-03-25 krauss 2011-03-25 eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
2011-03-25 bulwahn 2011-03-25 merged
2011-03-25 bulwahn 2011-03-25 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
2011-03-24 krauss 2011-03-24 added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
2011-03-24 krauss 2011-03-24 mira interface to 'isabelle make' in addition to usedir and makeall; do not require dependencies
2011-03-24 krauss 2011-03-24 clarified
2011-03-24 krauss 2011-03-24 parameterize configurations by custom settings
2011-03-25 noschinl 2011-03-25 Change coercion for RealDef to use function application (not composition)
2011-03-25 bulwahn 2011-03-25 revisiting Code_Prolog (cf. 6fe4abb9437b)
2011-03-25 bulwahn 2011-03-25 fixed postprocessing for term presentation in quickcheck; tuned spacing
2011-03-24 krauss 2011-03-24 enable Z3 in the test configuration
2011-03-24 blanchet 2011-03-24 add "-?" to "nitrox" tool
2011-03-24 blanchet 2011-03-24 clean up new Skolemizer code -- some old hacks are no longer necessary
2011-03-24 blanchet 2011-03-24 specify proper defaults for Nitpick and Refute on TPTP + tuning
2011-03-24 blanchet 2011-03-24 added "nitrox" tool (Nitpick for first-order TPTP problems) to components
2011-03-24 blanchet 2011-03-24 made one more Metis example use the new Skolemizer
2011-03-24 blanchet 2011-03-24 Metis examples use the new Skolemizer to test it
2011-03-24 blanchet 2011-03-24 new version of Metis 2.3 (29 Dec. 2010)
2011-03-24 blanchet 2011-03-24 remove newly added wrong logic
2011-03-24 blanchet 2011-03-24 more precise failure reporting in Sledgehammer/SMT
2011-03-24 blanchet 2011-03-24 avoid evil "export_without_context", which breaks if there are local "fixes"
2011-03-24 blanchet 2011-03-24 more robust handling of variables in new Skolemizer
2011-03-24 haftmann 2011-03-24 merged
2011-03-24 haftmann 2011-03-24 added subsection on Scala specialities
2011-03-24 krauss 2011-03-24 added more judgement day provers
2011-03-24 bulwahn 2011-03-24 allowing special set comprehensions in values command; adding an example for special set comprehension in values
2011-03-24 bulwahn 2011-03-24 merged
2011-03-23 bulwahn 2011-03-23 adding documentation about the eval option in quickcheck
2011-03-23 bulwahn 2011-03-23 adapting Quickcheck_Prolog to latest changes
2011-03-23 bulwahn 2011-03-23 changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
2011-03-23 bulwahn 2011-03-23 adapting mutabelle; exporting more Quickcheck functions
2011-03-23 bulwahn 2011-03-23 making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
2011-03-23 bulwahn 2011-03-23 changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout
2011-03-26 wenzelm 2011-03-26 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent; recovered printing of Hoare assign statements from 45d090186bbe;
2011-03-26 wenzelm 2011-03-26 tuned;
2011-03-26 wenzelm 2011-03-26 dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;