isabelle: Graph

modernized Quantifier1 simproc setup;
2011-04-22, by wenzelm
tuned signature;
2011-04-22, by wenzelm
clarified simpset setup;
2011-04-22, by wenzelm
iterate the unsound-fact-set removal process to recover even more unsound proofs
2011-04-22, by blanchet
automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
2011-04-22, by blanchet
automatically retry with full-types upon unsound proof
2011-04-21, by blanchet
detect some unsound proofs before showing them to the user
2011-04-21, by blanchet
tuning -- local semicolon consistency
2011-04-21, by blanchet
tuning
2011-04-21, by blanchet
rewording
2011-04-21, by blanchet
fixed interaction between monomorphization and slicing for ATPs
2011-04-21, by blanchet
cleanup: get rid of "may_slice" arguments without changing semantics
2011-04-21, by blanchet
implemented general slicing for ATPs, especially E 1.2w and above
2011-04-21, by blanchet
fixed typo in documentation
2011-04-21, by blanchet
more robust scanning of iterated comments, such as "(* (**) (**) *)";
2011-04-21, by wenzelm
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
2011-04-21, by wenzelm
eliminated Display.string_of_thm_without_context;
2011-04-20, by wenzelm
merged;
2011-04-20, by wenzelm
merged
2011-04-20, by blanchet
worked around Kodkodi limitation with parsing {}, where it cannot easily deduce its arity -- without this workaround, Kodkod sometimes generates arity errors in conjunction with the "need" option since change 614ff13dc5d2
2011-04-20, by blanchet
adding two further code-generator internal constants to the blacklist of Mutabelle
2011-04-20, by bulwahn
adding examples for Quickcheck used within locales
2011-04-20, by bulwahn
handling the case where quickcheck is used in a locale with no known interpretation user-friendly
2011-04-20, by bulwahn
added template diff against newer mercurials, where the 'ago' duplication has been fixed
2011-04-20, by krauss
use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations
2011-04-20, by krauss
hg template diff: renamed to reflect the base version (which silently changed in caf19101073d, by accident?)
2011-04-20, by krauss
standardized some ML aliases;
2011-04-20, by wenzelm
avoid Display.string_of_thm_without_context;
2011-04-20, by wenzelm
eliminated global references / critical sections via context data;
2011-04-20, by wenzelm
explicit context for Codegen.eval_term etc.;
2011-04-20, by wenzelm
added Theory.nodes_of convenience;
2011-04-20, by wenzelm
updated reference machines;
2011-04-20, by wenzelm
migrated macbroy6 to macbroy30, which is the new "mobile" server (2 cores, 4 GB, Mac OS 10.5);
2011-04-20, by wenzelm
merged
2011-04-20, by wenzelm
increase "auto"'s timeout in example to help SML/NJ
2011-04-20, by blanchet
making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement
2011-04-20, by bulwahn
merged
2011-04-19, by blanchet
avoid relying on "Thm.definitionK" to pick up definitions -- this was an old hack related to locales (to avoid expanding locale constants to their low-level definition) that is no longer necessary
2011-04-19, by blanchet
merged
2011-04-19, by berghofe
- renamed enum type class to spark_enum, to avoid confusion with
2011-04-19, by berghofe
use "Spec_Rules" for finding axioms -- more reliable and cleaner
2011-04-19, by blanchet
optimize trivial equalities early in Nitpick -- it shouldn't be the job of the peephole optimizer
2011-04-19, by blanchet
remove a few Nitpick calls in examples -- another step toward making them run faster
2011-04-19, by blanchet
check arity of bound variables to avoid generating too large Kodkod problems -- an issue that arose in the context of TPTP/CASC
2011-04-19, by blanchet
eliminated Codegen.mode in favour of explicit argument;
2011-04-19, by wenzelm
less bulky "_position", for improved readability of parse trees;
2011-04-19, by wenzelm
added more elementary Skip_Proof.make_thm_cterm;
2011-04-19, by wenzelm
explicit markup for loose bounds;
2011-04-19, by wenzelm
prefer internal types, via Simple_Syntax.read_typ;
2011-04-19, by wenzelm
eliminated obsolete Proof_Syntax.strip_sorts_consttypes;
2011-04-19, by wenzelm
split Type_Infer into early and late part, after Proof_Context;
2011-04-19, by wenzelm
minor tuning and modernization;
2011-04-19, by wenzelm
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
2011-04-19, by wenzelm
simplified check/uncheck interfaces: result comparison is hardwired by default;
2011-04-19, by wenzelm
updated some theory primitives, which now depend on auxiliary context;
2011-04-19, by wenzelm
more precise treatment of existing type inference parameters;
2011-04-19, by wenzelm
pretty_abbrev: read abbreviation more directly;
2011-04-18, by wenzelm
tuned signature;
2011-04-18, by wenzelm
raised timeouts further, for SML/NJ!
2011-04-18, by krauss
Package prefix is now taken into account when looking up user-defined
2011-04-18, by berghofe
merged
2011-04-18, by wenzelm
recovered Theory.check_def: full name needs to be determined from background thy, not auxiliary ctxt (broken in 774df7c59508, caused Nitpick.all_axioms_of to produce bad results);
2011-04-18, by wenzelm
scheduler for Mutabelle regression
2011-04-18, by krauss
tool for importing nightly isatest logs
2011-04-18, by krauss
adding bounded_forall tester
2011-04-18, by bulwahn
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
2011-04-18, by bulwahn
pass plain Proof.context for pretty printing;
2011-04-18, by wenzelm
standardized aliases of operations on tsig;
2011-04-18, by wenzelm
pass plain Proof.context for pretty printing;
2011-04-18, by wenzelm
tuned;
2011-04-18, by wenzelm
simplified Sorts.class_error: plain Proof.context;
2011-04-18, by wenzelm
pass plain Proof.context for pretty printing;
2011-04-18, by wenzelm
simplified pretty printing context, which is only required for certain kernel operations;
2011-04-18, by wenzelm
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
2011-04-17, by wenzelm
added Binding.print convenience, which includes quote already;
2011-04-17, by wenzelm
markup attributes/methods via name space;
2011-04-17, by wenzelm
tuned signature;
2011-04-17, by wenzelm
markup facts via name space;
2011-04-17, by wenzelm
tuned -- order in memory according to variance;
2011-04-17, by wenzelm
eliminated obsolete markup -- superseded by generic "entity" markup;
2011-04-17, by wenzelm
report Name_Space.declare/define, relatively to context;
2011-04-17, by wenzelm
clarified pretty_parsetree: suppress literal tokens;
2011-04-17, by wenzelm
PARALLEL_GOALS for simplification within auto_tac;
2011-04-16, by wenzelm
PARALLEL_GOALS for method "simp_all";
2011-04-16, by wenzelm
enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
2011-04-16, by wenzelm
refined PARALLEL_GOALS;
2011-04-16, by wenzelm
tuned blast: navigate to subgoal only once;
2011-04-16, by wenzelm
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
2011-04-16, by wenzelm
more direct Thm.cprem_of (with exception THM instead of Subscript);
2011-04-16, by wenzelm
more direct Thm.cprem_of (with exception THM instead of Subscript);
2011-04-16, by wenzelm
more direct Logic.dest_implies (with exception TERM instead of Subscript);
2011-04-16, by wenzelm
eliminated old List.nth;
2011-04-16, by wenzelm
do not open ML structures;
2011-04-16, by wenzelm
observe firm naming convention ctxt: Proof.context;
2011-04-16, by wenzelm
modernized structure Proof_Context;
2011-04-16, by wenzelm
modernized structure Proof_Context;
2011-04-16, by wenzelm
prefer local name spaces;
2011-04-16, by wenzelm
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-16, by wenzelm
tuned signature, disentangled dependencies;
2011-04-16, by wenzelm
Added command for associating user-defined types with SPARK types.
2011-04-15, by berghofe
turn YXML.parse_file into a fold
2011-04-14, by noschinl
nicer error message from Metis for know failure that isn't the user's fault
2011-04-14, by blanchet
correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
2011-04-14, by blanchet
tuning
2011-04-14, by blanchet
remove needless export
2011-04-14, by blanchet
more clausification tests
2011-04-14, by blanchet
make 48170228f562 work also with "HO_Reas" examples
2011-04-14, by blanchet
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
2011-04-14, by blanchet
properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
2011-04-14, by blanchet
remove experimental code added in 85bb6fbb8e6a
2011-04-14, by blanchet
added examples of definitional CNF facts
2011-04-14, by blanchet
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
2011-04-14, by blanchet
compile
2011-04-14, by blanchet
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
2011-04-14, by blanchet
removed obsolete Skolem counter in new Skolemizer
2011-04-14, by blanchet
added outstanding issue to Metis example
2011-04-14, by blanchet
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
2011-04-14, by blanchet
started clausifier examples
2011-04-14, by blanchet
make new Skolemizer work also for "metisFT"
2011-04-14, by blanchet
improve definitional CNF on goal by moving "not" past the quantifiers
2011-04-14, by blanchet
experiment with definitional CNF
2011-04-14, by blanchet
use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer
2011-04-14, by blanchet
try to repair out-of-sync situations in Metis
2011-04-14, by blanchet
handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used
2011-04-14, by blanchet
Add YXML.parse_file to signature ...
2011-04-13, by noschinl
Add YXML.parse_file to parse and process big data files
2011-04-13, by noschinl
Generalized File.fold_lines to File.fold_fields
2011-04-13, by noschinl
more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;
2011-04-11, by wenzelm
Name_Space.entry_markup: keep def position as separate properties;
2011-04-11, by wenzelm
some position reports for 'translations';
2011-04-09, by wenzelm
made SML/NJ happy;
2011-04-09, by wenzelm
merged
2011-04-09, by wenzelm
added SMT certificates
2011-04-08, by boehmes
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
2011-04-08, by boehmes
fixed eta-expansion: use correct order to apply new bound variables
2011-04-08, by boehmes
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
2011-04-08, by boehmes
unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
2011-04-08, by boehmes
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
2011-04-08, by boehmes
merged
2011-04-08, by bulwahn
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
2011-04-08, by bulwahn
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
2011-04-08, by bulwahn
correcting constant name in exhaustive_generators
2011-04-08, by bulwahn
switching fast compilation off by default for now in exhaustive quickcheck
2011-04-08, by bulwahn
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
2011-04-08, by bulwahn
rational and real instances for new compilation scheme for exhaustive quickcheck
2011-04-08, by bulwahn
splitting exhaustive and full_exhaustive into separate type classes
2011-04-08, by bulwahn
removing duplicate code
2011-04-08, by bulwahn
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
2011-04-08, by bulwahn
creating a general mk_equation_terms for the different compilations
2011-04-08, by bulwahn
adding an even faster compilation scheme
2011-04-08, by bulwahn
theory definitions for fast exhaustive quickcheck compilation
2011-04-08, by bulwahn
new compilation for exhaustive quickcheck
2011-04-08, by bulwahn
tuned;
2011-04-08, by wenzelm
present type variables;
2011-04-08, by wenzelm
unparse: more accurate markup for syntax consts, notably binders;
2011-04-08, by wenzelm
notation: proper markup for type constructor / constant;
2011-04-08, by wenzelm
tuned signature;
2011-04-08, by wenzelm
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
2011-04-08, by wenzelm
discontinued Syntax.max_pri, which is not really a symbolic parameter;
2011-04-08, by wenzelm
CONST syntax with positions;
2011-04-08, by wenzelm
moved CONST syntax/translations to their proper place;
2011-04-08, by wenzelm
simplified Pure syntax bootstrap;
2011-04-08, by wenzelm
renamed sprop "prop#" to "prop'" -- proper identifier;
2011-04-08, by wenzelm
merged
2011-04-08, by wenzelm
raised timeout further, for SML/NJ
2011-04-07, by krauss
discontinued special treatment of structure Lexicon;
2011-04-08, by wenzelm
discontinued special status of structure Printer;
2011-04-08, by wenzelm
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
2011-04-08, by wenzelm
discontinued special treatment of structure Mixfix;
2011-04-08, by wenzelm
more antiquotations;
2011-04-08, by wenzelm
removed outdated text (cf. 84a3f86441eb);
2011-04-08, by wenzelm
explicit structure Syntax_Trans;
2011-04-08, by wenzelm
tuned presentation;
2011-04-08, by wenzelm
report literal tokens according to parsetree head;
2011-04-07, by wenzelm
simplified read_term vs. read_prop;
2011-04-07, by wenzelm
tuned signature;
2011-04-07, by wenzelm
constant =?= no longer exists (cf. 8c09e1fa24a7);
2011-04-07, by wenzelm
clarified sources -- removed odd comments;
2011-04-07, by wenzelm
tuned signature;
2011-04-07, by wenzelm
merged
2011-04-07, by wenzelm
removing decrement of cardinality in quickcheck -- counting cardinalities starts at 1
2011-04-07, by bulwahn
removing instantiation exhaustive for unit in Quickcheck_Exhaustive
2011-04-07, by bulwahn
correcting bounded_forall construction; tuned
2011-04-07, by bulwahn
dropped unused lemmas; proper Isar proof
2011-04-07, by haftmann
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
2011-04-07, by blanchet
make new Skolemizer more robust
2011-04-07, by blanchet
tuned comment
2011-04-07, by blanchet
discontinued user-defined token translations;
2011-04-07, by wenzelm
simplified printer context: uniform externing and static token translations;
2011-04-07, by wenzelm
clarified Pretty.mark;
2011-04-07, by wenzelm
parallel parsing of big specifications;
2011-04-06, by wenzelm
separate structure Term_Position;
2011-04-06, by wenzelm
type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);
2011-04-06, by wenzelm
moved type syntax translations to syn_trans.ML;
2011-04-06, by wenzelm
made SML/NJ happy (cf. 578a51fae383);
2011-04-06, by wenzelm
merged
2011-04-06, by wenzelm
merged
2011-04-06, by bulwahn
changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
2011-04-06, by bulwahn
prove measurable_into_infprod_algebra and measure_infprod
2011-04-05, by hoelzl
Rename extensional to extensionalD (extensional is also defined in FuncSet)
2011-04-05, by hoelzl
eliminated slightly odd Syntax.rep_syntax;
2011-04-06, by wenzelm
more abstract print translation;
2011-04-06, by wenzelm
more abstract syntax translation;
2011-04-06, by wenzelm
tuned;
2011-04-06, by wenzelm
explicit Syntax.tokenize, Syntax.parse;
2011-04-06, by wenzelm
eliminated odd object-oriented type_context/term_context;
2011-04-06, by wenzelm
simplified standard parse/unparse;
2011-04-06, by wenzelm
discontinued old-style Syntax.constrainC;
2011-04-06, by wenzelm
typed_print_translation: discontinued show_sorts argument;
2011-04-06, by wenzelm
misc tuning and simplification;
2011-04-06, by wenzelm
moved unparse material to syntax_phases.ML;
2011-04-06, by wenzelm
more symbol abbrevs;
2011-04-06, by wenzelm
renamed Standard_Syntax to Syntax_Phases;
2011-04-06, by wenzelm
moved decode/parse operations to standard_syntax.ML;
2011-04-05, by wenzelm
separate module for standard implementation of inner syntax operations;
2011-04-05, by wenzelm
moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
2011-04-05, by wenzelm
merged
2011-04-05, by wenzelm
added "no_atp" to Cantor's paradox
2011-04-05, by blanchet
renamed "const_args" option value to "args"
2011-04-05, by blanchet
temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception
2011-04-05, by blanchet
updated instructions
2011-04-05, by blanchet
minor doc edits
2011-04-05, by blanchet
killed unimplemented type encoding "preds"
2011-04-05, by blanchet
remove debugging code
2011-04-05, by blanchet
removing bounded_forall code equation for characters when loading Code_Char
2011-04-05, by bulwahn
deriving bounded_forall instances in quickcheck_exhaustive
2011-04-05, by bulwahn
generalizing ensure_sort_datatype for bounded_forall instances
2011-04-05, by bulwahn
document "type_sys" option
2011-04-04, by blanchet
if "monomorphize" is enabled, mangle the type information in the names by default
2011-04-04, by blanchet
use standard tables with standard argument order;
2011-04-05, by wenzelm
discontinued special treatment of structure Parser -- directly accessible;
2011-04-05, by wenzelm
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-05, by wenzelm
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
Metis examples use the new Skolemizer to test it
2011-03-24, by blanchet
new version of Metis 2.3 (29 Dec. 2010)
2011-03-24, by blanchet
remove newly added wrong logic
2011-03-24, by blanchet
more precise failure reporting in Sledgehammer/SMT
2011-03-24, by blanchet
avoid evil "export_without_context", which breaks if there are local "fixes"
2011-03-24, by blanchet
more robust handling of variables in new Skolemizer
2011-03-24, by blanchet
merged
2011-03-24, by haftmann
added subsection on Scala specialities
2011-03-24, by haftmann
added more judgement day provers
2011-03-24, by krauss
allowing special set comprehensions in values command; adding an example for special set comprehension in values
2011-03-24, by bulwahn
merged
2011-03-24, by bulwahn
adding documentation about the eval option in quickcheck
2011-03-23, by bulwahn
adapting Quickcheck_Prolog to latest changes
2011-03-23, by bulwahn
changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
2011-03-23, by bulwahn
adapting mutabelle; exporting more Quickcheck functions
2011-03-23, by bulwahn
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, by bulwahn
changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout
2011-03-23, by bulwahn
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
2011-03-26, by wenzelm
tuned;
2011-03-26, by wenzelm
dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;
2011-03-26, by wenzelm
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2011-03-24, by wenzelm
more direct loose_bvar1;
2011-03-24, by wenzelm
indentation;
2011-03-24, by wenzelm
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
2011-03-24, by wenzelm
added editor mode line;
2011-03-23, by wenzelm
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
2011-03-23, by wenzelm
list Isabelle tools via perl script, which is much faster that bash plumbing, especially on Cygwin;
2011-03-23, by wenzelm
updated contributed components
2011-03-23, by boehmes
Z3 non-commercial usage may explicitly be declined
2011-03-23, by boehmes
export status function to query whether Z3 has been activated for usage within Isabelle
2011-03-23, by boehmes
merge
2011-03-23, by blanchet
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
2011-03-23, by blanchet