isabelle: Graph

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