isabelle: Graph

don't report spurious LEO-II errors
2012-02-14, by blanchet
better error message
2012-02-14, by blanchet
removing debug code in mutabelle
2012-02-14, by bulwahn
adding abort_potential functionality in quickcheck
2012-02-14, by bulwahn
adding abort_potential configuration in Quickcheck
2012-02-14, by bulwahn
clarified bires_inst_tac: retain internal exceptions;
2012-02-14, by wenzelm
tuned signature;
2012-02-14, by wenzelm
more conventional tactic setup -- avoid low-level Thm.dest_state and spurious warnings about it;
2012-02-14, by wenzelm
more conventional tactic setup;
2012-02-14, by wenzelm
eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);
2012-02-14, by wenzelm
prefer high-level elim_format;
2012-02-14, by wenzelm
discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;
2012-02-14, by wenzelm
method setup;
2012-02-14, by wenzelm
simplified use of tacticals;
2012-02-14, by wenzelm
comment;
2012-02-14, by wenzelm
tuned signature, according to actual usage of these operations;
2012-02-14, by wenzelm
tuned signature;
2012-02-14, by wenzelm
normalized aliases;
2012-02-14, by wenzelm
elininated unused INTLEAVE;
2012-02-14, by wenzelm
eliminated unused rewrite_goal_rule;
2012-02-14, by wenzelm
eliminated unused subgoals_tac;
2012-02-14, by wenzelm
eliminated obsolete aliases;
2012-02-14, by wenzelm
eliminated obsolete aliases;
2012-02-14, by wenzelm
tuned;
2012-02-14, by wenzelm
merged, resolving trivial conflicts;
2012-02-14, by wenzelm
merged;
2012-02-14, by wenzelm
new SPASS options
2012-02-11, by blanchet
making num_mutations a configuration that can be changed with the mutabelle bash command
2012-02-11, by bulwahn
making max_mutants an option that can be changed in the Mutabelle-script
2012-02-11, by bulwahn
increase timeout to 30 seconds; changing mutabelle script
2012-02-11, by bulwahn
parse clauses generated from several formulas
2012-02-10, by blanchet
be more gentle when generating KBO weights
2012-02-10, by blanchet
update SPASS slices
2012-02-10, by blanchet
more specification of the quotient package in IsarRef
2012-02-10, by Cezary Kaliszyk
specification of the quotient package
2012-02-10, by Cezary Kaliszyk
tune KBO weight code
2012-02-09, by blanchet
minor DFG fix
2012-02-09, by blanchet
new SPASS slices
2012-02-09, by blanchet
improved KBO weights -- beware of explicit applications
2012-02-09, by blanchet
added possibility of generating KBO weights to DFG problems
2012-02-09, by blanchet
Generalize the compositional preservation theorems
2012-02-09, by Cezary Kaliszyk
use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
2012-02-08, by blanchet
removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
2012-02-08, by blanchet
beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms
2012-02-08, by blanchet
fixed arity error
2012-02-06, by blanchet
tuning
2012-02-06, by blanchet
renamed type encoding
2012-02-06, by blanchet
adding some forbidden constant names for mutabelle
2012-02-05, by bulwahn
mutabelle ignores theorems with internal constants
2012-02-05, by bulwahn
tuned
2012-02-05, by nipkow
merged
2012-02-05, by nipkow
simplified code generation
2012-02-05, by nipkow
remove option that's on by default
2012-02-05, by blanchet
no need for a script/mega-hack with the new SPASS
2012-02-05, by blanchet
cleaned up new SPASS parsing
2012-02-05, by blanchet
tuning
2012-02-05, by blanchet
merged
2012-02-05, by bulwahn
adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
2012-02-05, by bulwahn
tuning to remove ML warnings
2012-02-05, by bulwahn
removed double filtering of type args
2012-02-05, by blanchet
adding a quickcheck example about functions and sets
2012-02-05, by bulwahn
removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)
2012-02-05, by bulwahn
adding a remark about lemma which is too special and should be removed
2012-02-05, by bulwahn
another try to improve code generation of set equality (cf. da32cf32c0c7)
2012-02-05, by bulwahn
beautifying definitions of check_all and adding instance for finite_4
2012-02-05, by bulwahn
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
2012-02-05, by Cezary Kaliszyk
added option to Mirabelle/Sledgehammer
2012-02-04, by blanchet
improved hashing w.r.t. Mirabelle, to help debugging
2012-02-04, by blanchet
tuned SPASS DFG output
2012-02-04, by blanchet
the new SPASS gives accurate fact information, so no need for old hack anymore
2012-02-04, by blanchet
fixed docs
2012-02-04, by blanchet
made sure to filter type args also for "uncurried alias" equations
2012-02-04, by blanchet
made option available to users (mostly for experiments)
2012-02-04, by blanchet
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)
2012-02-04, by bulwahn
optimization: slice caching in case two consecutive slices are nearly identical
2012-02-03, by blanchet
extended SPASS/DFG output with ranks
2012-02-03, by blanchet
try to pass fewer options to Metis
2012-02-03, by blanchet
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
2012-02-03, by Cezary Kaliszyk
improve SPASS scripts
2012-02-02, by blanchet
change 9ce354a77908 wasn't quite right -- here's an improvement
2012-02-02, by blanchet
better SPASS setup
2012-02-02, by blanchet
don't introduce new symbols in helpers -- makes problems unprovable
2012-02-02, by blanchet
only constants can be aliased
2012-02-02, by blanchet
include new SPASS by default if available
2012-02-02, by blanchet
adding an example for finite and cofinite sets
2012-02-02, by bulwahn
adding a minimally refined equality on sets for code generation
2012-02-02, by bulwahn
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
2012-02-02, by bulwahn
improving code equations for multisets that violated the distinct AList abstraction
2012-02-01, by bulwahn
tuning
2012-02-02, by blanchet
implemented partial application aliases (for SPASS mainly)
2012-02-02, by blanchet
really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
2012-02-01, by blanchet
don't stumble on SPASS debug output
2012-02-01, by blanchet
tuning
2012-02-01, by blanchet
proper statuses for "fact_from_ref"
2012-02-01, by blanchet
tuned
2012-01-31, by nipkow
renamed Sledgehammer option
2012-01-31, by blanchet
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
2012-01-31, by blanchet
improve SPASS setup
2012-01-31, by blanchet
adding code equation for setsum
2012-01-31, by bulwahn
avoid name clash, really
2012-01-31, by blanchet
fixed syntax bug in DFG output
2012-01-31, by blanchet
new SPASS setup
2012-01-31, by blanchet
distinguish between ":lr" and ":lt" (terminating) in DFG format
2012-01-31, by blanchet
nicer keyword class avoidance scheme
2012-01-31, by blanchet
new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)
2012-01-31, by blanchet
mutabelle must handle the case where quickcheck returns multiple results
2012-01-31, by bulwahn
reverted e2b1a86d59fc -- broke Metis's lambda-lifting
2012-01-31, by blanchet
merged
2012-01-31, by nipkow
NEWS
2012-01-31, by nipkow
added "'a rel"
2012-01-30, by nipkow
fix debilitating bug with lambda lifting in conjectures with outer existential quantifiers
2012-01-30, by blanchet
new SPASS setup
2012-01-30, by blanchet
example tuning
2012-01-30, by blanchet
implemented new lambda translations scheme
2012-01-30, by blanchet
avoid unsupported case in Metis
2012-01-30, by blanchet
docs and news
2012-01-30, by blanchet
rename lambda translation schemes
2012-01-30, by blanchet
example tuning
2012-01-30, by blanchet
NEWS
2012-01-30, by bulwahn
renaming all lemmas with name rel_pow to relpow
2012-01-30, by bulwahn
adding code equations for max_extp and mlex
2012-01-30, by bulwahn
adding code generation for relpow by copying the ideas for code generation of funpow
2012-01-30, by bulwahn
adding code equation for rtranclp in Enum
2012-01-30, by bulwahn
adding code equation for max_ext
2012-01-30, by bulwahn
adding code equation for tranclp
2012-01-30, by bulwahn
adding code_unfold to make measure executable
2012-01-30, by bulwahn
removed accidental dependance of abstract interpreter on gamma
2012-01-29, by nipkow
merged
2012-01-29, by nipkow
tuned
2012-01-29, by nipkow
an executable version of accessible part (only for finite types yet)
2012-01-28, by bulwahn
adding yet another induction rule on natural numbers
2012-01-28, by bulwahn
moving declarations back to the section they seem to belong to (cf. afffe1f72143)
2012-01-28, by bulwahn
reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
2012-01-28, by bulwahn
adding some more examples for quickcheck; replaced FIXME comments
2012-01-27, by bulwahn
new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well
2012-01-27, by bulwahn
removed duplicate definitions that made locale inconsistent
2012-01-27, by nipkow
added parity analysis
2012-01-27, by nipkow
corrected expectation; added an example for quickcheck
2012-01-27, by bulwahn
adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck
2012-01-27, by bulwahn
made SML/NJ happy
2012-01-27, by blanchet
even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant
2012-01-26, by blanchet
separate orthogonal components
2012-01-26, by blanchet
generate left-to-right rewrite tag for combinator helpers for SPASS 3.8
2012-01-26, by blanchet
better handling of individual type for DFG format (SPASS)
2012-01-26, by blanchet
adding quickcheck example with THE
2012-01-26, by bulwahn
evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
2012-01-26, by bulwahn
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4
2012-01-26, by bulwahn
tuned
2012-01-26, by nipkow
adding very basic code generation to Wellfounded theory
2012-01-25, by bulwahn
removing dead code from Mutabelle; tuned
2012-01-25, by bulwahn
generalizing check if size matters because it is different for random and exhaustive testing
2012-01-25, by bulwahn
merged
2012-01-25, by bulwahn
adding code equation for Collect on finite types
2012-01-25, by bulwahn
Use lookup_size rather than Datatype.get_info in is_poly to avoid
2012-01-24, by berghofe
adding some rules to quickcheck's preprocessing
2012-01-24, by bulwahn
some more constants on mutabelle's blacklist
2012-01-24, by bulwahn
implemented "tptp_refute" tool
2012-01-23, by blanchet
added problem importer
2012-01-23, by blanchet
imported patch ATP_Problem_Import.thy
2012-01-23, by blanchet
imported patch atp_problem_import.ML
2012-01-23, by blanchet
renamed theory exporter
2012-01-23, by blanchet
renamed two files to make room for a new file
2012-01-23, by blanchet
rebranded Nitrox, for more uniformity
2012-01-23, by blanchet
moved "nitrox" to TPTP
2012-01-23, by blanchet
generalize type of List.listrel
2012-01-23, by huffman
support for Ex1 in quickcheck-narrowing
2012-01-23, by bulwahn
adding another internal constant to mutabelle's blacklust
2012-01-23, by bulwahn
adding some more forbidden constant names for the mutated conjecture generation
2012-01-23, by bulwahn
adding code generation for some list relations
2012-01-23, by bulwahn
adding fun_eq_iff to the preprocessing
2012-01-23, by bulwahn
random instance for sets
2012-01-23, by bulwahn
more configurations to mutabelle
2012-01-23, by bulwahn
catching code generation errors in quickcheck-narrowing
2012-01-20, by bulwahn
adding narrowing instance for sets
2012-01-20, by bulwahn
shortened definitions by adding some termify constants
2012-01-20, by bulwahn
tuned
2012-01-20, by bulwahn
adding check_all instance for sets; tuned
2012-01-20, by bulwahn
tuned
2012-01-20, by nipkow
tuned
2012-01-20, by nipkow
minor edits in docs
2012-01-19, by blanchet
renamed "sound" option to "strict"
2012-01-19, by blanchet
updated Sledge docs some more
2012-01-19, by blanchet
more doc updates
2012-01-19, by blanchet
updated docs
2012-01-19, by blanchet
lower timeout for preplay, now that we have more preplay methods
2012-01-19, by blanchet
cleanly separate each Metis encoding
2012-01-19, by blanchet
basic setup for equational reasoning;
2012-02-09, by wenzelm
tuned;
2012-02-07, by wenzelm
updated examples for syntax translations;
2012-02-07, by wenzelm
updated section on raw syntax;
2012-02-05, by wenzelm
updated section about syntax ambiguity;
2012-02-05, by wenzelm
updated/unified section on mixfix annotations;
2012-02-04, by wenzelm
tuned;
2012-02-04, by wenzelm
more on explicit notation;
2012-02-04, by wenzelm
more accurate Pure grammar;
2012-02-04, by wenzelm
more refs;
2012-02-04, by wenzelm
simplified mixfix (NB: infix is no longer required separately);
2012-02-04, by wenzelm
updated section on print modes;
2012-02-02, by wenzelm
misc tuning and reformatting;
2012-02-02, by wenzelm
clarified syntax section structure;
2012-02-02, by wenzelm
discontinued obscure history commands;
2012-02-02, by wenzelm
misc tuning and reformatting;
2012-02-02, by wenzelm
discontinued obscure history commands;
2012-02-02, by wenzelm
updated hint about asm_rl;
2012-01-29, by wenzelm
updated thin_tac;
2012-01-29, by wenzelm
updated distinct_subgoals_tac, flexflex_tac;
2012-01-29, by wenzelm
removed obscure material;
2012-01-29, by wenzelm
updated rotate_tac;
2012-01-29, by wenzelm
tuned;
2012-01-27, by wenzelm
updated citations;
2012-01-27, by wenzelm
updated subgoal_tac;
2012-01-27, by wenzelm
tuned sectioning;
2012-01-26, by wenzelm
updated "Control and search tacticals" (moved from ref to implementation);
2012-01-26, by wenzelm
obsolete -- covered in implementation manual;
2012-01-26, by wenzelm
moved HEADGOAL;
2012-01-26, by wenzelm
removed some obscure material;
2012-01-26, by wenzelm
added SELECT_GOAL;
2012-01-26, by wenzelm
tuned;
2012-01-26, by wenzelm
updated "subgoal quantifiers";
2012-01-25, by wenzelm
tuned ML infixes;
2012-01-25, by wenzelm
document antiquotations for ML infix operators;
2012-01-25, by wenzelm
tuned;
2012-01-25, by wenzelm
updated repetition tacticals;
2012-01-25, by wenzelm
updated THEN, ORELSE, APPEND, and derivatives;
2012-01-25, by wenzelm
removed obscure/outdated material;
2012-01-25, by wenzelm
updated RSN, RL, RLN, MRS;
2012-01-25, by wenzelm
removed obscure/outdated material;
2012-01-25, by wenzelm
tuned;
2012-01-25, by wenzelm
more on Logic.all/mk_implies etc.;
2012-01-25, by wenzelm
reduce AFP test by many hours;
2012-01-19, by wenzelm
added termination of narrowing
2012-01-19, by nipkow
really need 64bit here;
2012-01-18, by wenzelm
Added termination proof for widening
2012-01-18, by nipkow
switch afp test to Darwin on macbroy2
2012-01-18, by kleing
merged
2012-01-18, by nipkow
introduced commands over a set of vars
2012-01-18, by nipkow
basic support for PIDE Scala programming, independently of the main Isabelle repository;
2012-01-18, by wenzelm
fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick
2012-01-17, by blanchet
updated message
2012-01-17, by blanchet
improve installation instructions
2012-01-17, by blanchet