isabelle: Graph

more precise propagation of reports/results through some inner syntax layers;
2011-04-05, by wenzelm
accumulate parsetrees in canonical reverse order;
2011-04-04, by wenzelm
tuned;
2011-04-04, by wenzelm
tuned -- removed redundancy;
2011-04-04, by wenzelm
tuned signatures;
2011-04-04, by wenzelm
streamlined token list operations, assuming that the order of union does not matter;
2011-04-04, by wenzelm
misc tuning and clarification;
2011-04-04, by wenzelm
merged
2011-04-04, by wenzelm
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
2011-04-04, by blanchet
refactoring generator definition in quickcheck and removing clone
2011-04-04, by bulwahn
use the proper contexts/simpsets/etc. in the TPTP proof method
2011-04-04, by blanchet
merged
2011-04-04, by blanchet
make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option
2011-04-04, by blanchet
merged
2011-04-04, by paulson
Deletion of all semicolons, because they interfere with Proof General
2011-04-04, by paulson
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
2011-04-04, by krauss
tuned proofs
2011-04-03, by haftmann
tuned proof
2011-04-02, by haftmann
direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;
2011-04-04, by wenzelm
added Position.reports convenience;
2011-04-03, by wenzelm
show more tooltip/sub-expression markup;
2011-04-03, by wenzelm
show tooltip/sub-expression for entity markup;
2011-04-03, by wenzelm
merged
2011-04-01, by wenzelm
remove unnecessary prob_preserving
2011-04-01, by hoelzl
add prob_space_vimage
2011-04-01, by hoelzl
use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);
2011-04-01, by wenzelm
fixed accidental redefinition
2011-04-01, by krauss
save reflexivity steps in discharging Z3 Skolemization hypotheses
2011-04-01, by boehmes
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
2011-04-01, by bulwahn
adding general interface for batch validators in quickcheck
2011-04-01, by bulwahn
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
2011-04-01, by blanchet
scheduler for judgement day
2011-04-01, by krauss
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
2011-04-01, by boehmes
make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
2011-04-01, by boehmes
merged
2011-04-01, by bulwahn
adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
2011-04-01, by bulwahn
raised timeouts further, for SML/NJ
2011-04-01, by krauss
adapted parsing of session timing (cf. e86b10c68f0b)
2011-04-01, by krauss
merged
2011-03-31, by bulwahn
adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
2011-03-31, by bulwahn
provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
2011-03-31, by boehmes
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
2011-03-31, by blanchet
temporary workaround: filter out spurious monomorphic instances
2011-03-31, by blanchet
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-03-31, by blanchet
added support for "dest:" to "try"
2011-03-31, by blanchet
corrected infix precedence for boolean operators in Haskell
2011-03-31, by haftmann
merged
2011-03-31, by bulwahn
removing dead code in exhaustive_generators
2011-03-30, by bulwahn
removing junk that should not have been committed
2011-03-30, by bulwahn
modernized specifications;
2011-03-30, by wenzelm
accomodate autofix discipline of non-body context;
2011-03-30, by wenzelm
session timing: show pseudo-speedup factor;
2011-03-30, by wenzelm
visualize skolem and hilite (undeclared frees);
2011-03-30, by wenzelm
more informative markup_free;
2011-03-30, by wenzelm
inline lemmas instead of accidental physical addressing -- explicit is better than implicit;
2011-03-30, by wenzelm
tuned white space and indentation;
2011-03-30, by wenzelm
actually check list comprehension examples;
2011-03-30, by wenzelm
products of probability measures are probability measures
2011-03-30, by hoelzl
real multiplication is continuous
2011-03-30, by hoelzl
add lebesgue_real_affine
2011-03-30, by hoelzl
renewing specifications in HOL: replacing types by type_synonym
2011-03-30, by bulwahn
moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
2011-03-30, by bulwahn
adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape
2011-03-30, by bulwahn
NEWS
2011-03-30, by bulwahn
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
2011-03-30, by bulwahn
merged
2011-03-29, by wenzelm
added missing smlnj target
2011-03-29, by krauss
modernized specifications -- less axioms;
2011-03-29, by wenzelm
modernized specifications -- some attempts to avoid wild axiomatizations;
2011-03-29, by wenzelm
tuned proofs;
2011-03-29, by wenzelm
use shared copy of hoare_syntax.ML;
2011-03-29, by wenzelm
Hoare syntax: standard abstraction syntax admits source positions;
2011-03-29, by wenzelm
tuned headers;
2011-03-29, by wenzelm
tuned headers;
2011-03-29, by wenzelm
NEWS
2011-03-29, by hoelzl
rename Probability_Space to Probability_Measure
2011-03-29, by hoelzl
add infinite product measure
2011-03-29, by hoelzl
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
2011-03-29, by hoelzl
proved caratheodory_empty_continuous
2011-03-29, by hoelzl
list comprehension: strip positions where the translation cannot handle them right now;
2011-03-28, by wenzelm
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, by wenzelm
raised various timeouts to accommodate sluggish SML/NJ
2011-03-28, by krauss
changing values_timeout from a static option to a dynamic option as required for testing with SML/NJ
2011-03-28, by bulwahn
keep smlnj HOL images around
2011-03-28, by krauss
merged
2011-03-27, by wenzelm
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
2011-03-27, by krauss
avoid *** in normal output, which usually marks errors in logs
2011-03-27, by krauss
added Markup.Name and Markup.Kind convenience;
2011-03-27, by wenzelm
decode_term: some context-sensitive markup;
2011-03-27, by wenzelm
tuned signatures;
2011-03-27, by wenzelm
decode_term: more precise reports;
2011-03-27, by wenzelm
adhoc token style for free/bound;
2011-03-27, by wenzelm
decode_term/disambig: report resolved term variables for the unique (!) result;
2011-03-27, by wenzelm
removed unclear comments stemming from ed24ba6f69aa;
2011-03-27, by wenzelm
present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
2011-03-26, by wenzelm
added Future.cond_forks convenience;
2011-03-26, by wenzelm
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
2011-03-26, by wenzelm
tuned;
2011-03-26, by wenzelm
more direct loose_bvar1;
2011-03-26, by wenzelm
suppress Mercurial backup files;
2011-03-26, by wenzelm
updated generated file;
2011-03-26, by wenzelm
merged
2011-03-26, by wenzelm
SML_makeall: run with -j 3
2011-03-26, by krauss
fixed incomplete rename (1cdf54e845fa)
2011-03-25, by krauss
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
2011-03-25, by krauss
merged
2011-03-25, by bulwahn
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
2011-03-25, by bulwahn
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
2011-03-24, by krauss
mira interface to 'isabelle make' in addition to usedir and makeall;
2011-03-24, by krauss
clarified
2011-03-24, by krauss
parameterize configurations by custom settings
2011-03-24, by krauss
Change coercion for RealDef to use function application (not composition)
2011-03-25, by noschinl
revisiting Code_Prolog (cf. 6fe4abb9437b)
2011-03-25, by bulwahn
fixed postprocessing for term presentation in quickcheck; tuned spacing
2011-03-25, by bulwahn
enable Z3 in the test configuration
2011-03-24, by krauss
add "-?" to "nitrox" tool
2011-03-24, by blanchet
clean up new Skolemizer code -- some old hacks are no longer necessary
2011-03-24, by blanchet
specify proper defaults for Nitpick and Refute on TPTP + tuning
2011-03-24, by blanchet
added "nitrox" tool (Nitpick for first-order TPTP problems) to components
2011-03-24, by blanchet
made one more Metis example use the new Skolemizer
2011-03-24, by blanchet