isabelle: Graph

handle constructor syntax in n2m primcorec
2013-11-04, by blanchet
typo
2013-11-04, by blanchet
made sugared 'coinduct' theorem construction n2m-proof
2013-11-04, by blanchet
moved code around
2013-11-04, by blanchet
tuning
2013-11-04, by blanchet
make code more robust w.r.t. applied/unapplied map (primrec vs. primcorec)
2013-11-04, by blanchet
conceal definition
2013-11-04, by blanchet
more exercises
2013-11-02, by nipkow
more exercises
2013-11-02, by nipkow
more simplification rules on unary and binary minus
2013-11-01, by haftmann
generate stable names for axioms
2013-10-31, by blanchet
purely algebraic foundation for even/odd
2013-10-31, by haftmann
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
2013-10-31, by haftmann
explicit type class for modelling even/odd parity
2013-10-31, by haftmann
generalized of_bool conversion
2013-10-31, by haftmann
separated bit operations on type bit from generic syntactic bit operations
2013-10-31, by haftmann
restructed
2013-10-31, by haftmann
generalised lemma
2013-10-31, by haftmann
more lemmas on division
2013-10-31, by haftmann
more convenient place for a theory in solitariness
2013-10-31, by haftmann
consolidated clone theory
2013-10-31, by haftmann
more exercises
2013-10-31, by nipkow
tuned text
2013-10-30, by nipkow
inst_lift now fully instantiates context to avoid problems with loose bound variables
2013-10-29, by berghofe
include corecursive functions' arguments in callssss
2013-10-29, by panny
more exercises
2013-10-29, by nipkow
merged
2013-10-28, by nipkow
more exercises
2013-10-28, by nipkow
commented out vaporware
2013-10-27, by blanchet
more exercises
2013-10-26, by nipkow
tuning
2013-10-26, by blanchet
tuning
2013-10-26, by blanchet
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
2013-10-26, by blanchet
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
2013-10-26, by blanchet
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
2013-10-26, by blanchet
tuned error message
2013-10-26, by blanchet
more exercises
2013-10-25, by nipkow
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
2013-10-24, by blanchet
tuning
2013-10-24, by blanchet
more correct (!) types for recursive calls
2013-10-24, by blanchet
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
2013-10-24, by blanchet
got rid of annoying duplicate rewrite rule warnings
2013-10-24, by blanchet
use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
2013-10-24, by blanchet
refactored rtrancl_while; prove termination for finite rtrancl
2013-10-24, by traytel
more exercises
2013-10-23, by nipkow
added exercises
2013-10-23, by nipkow
added 'primcorec' examples
2013-10-23, by blanchet
tuned
2013-10-23, by nipkow
removed junk
2013-10-22, by traytel
update doc according to c0186a0d8cb3
2013-10-22, by traytel
define a trivial nonemptiness witness if none is provided
2013-10-22, by traytel
made lower-level function available
2013-10-21, by blanchet
more doc -- feedback from Andrei P.
2013-10-21, by blanchet
added exercise
2013-10-21, by nipkow
more docs
2013-10-21, by blanchet
more docs
2013-10-21, by blanchet
more docs
2013-10-21, by blanchet
expand doc a bit
2013-10-21, by blanchet
updated doc
2013-10-21, by blanchet
tuning
2013-10-21, by blanchet
warn about incompatible recursor signature
2013-10-21, by blanchet
more informative abort
2013-10-21, by blanchet
tuning
2013-10-21, by blanchet
systematically close derivations in BNF package
2013-10-21, by blanchet
removed temporary error handling
2013-10-20, by blanchet
strengthened tactic
2013-10-20, by blanchet
tuning
2013-10-20, by blanchet
reintroduced parts of 07a8145aaeba that a22ded8a7f7d wrongly took out
2013-10-20, by blanchet
tuning
2013-10-20, by blanchet
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
2013-10-20, by blanchet
tuning
2013-10-20, by blanchet
tuning
2013-10-20, by blanchet
tuning
2013-10-20, by blanchet
tuning
2013-10-20, by blanchet
simplify code
2013-10-20, by blanchet
avoid tactic failure for equations that contain an unapplied 'id'
2013-10-20, by blanchet
improve support for recursion through functions
2013-10-19, by blanchet
handle composition for multiple arguments correctly
2013-10-18, by blanchet
merge
2013-10-18, by panny
generate callssss
2013-10-18, by panny
set stage for more flexible 'primrec' syntax for recursion through functions
2013-10-18, by blanchet
don't print BNF constants
2013-10-18, by blanchet
tuning
2013-10-18, by blanchet
conceal even more ugly constructions
2013-10-18, by blanchet
conceal more ugly constructions
2013-10-18, by blanchet
conceal prim(co)rec definitions
2013-10-18, by blanchet
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
2013-10-18, by blanchet
updated docs
2013-10-18, by blanchet
set code attribute on discriminator equations
2013-10-18, by blanchet
MaSh error handling
2013-10-18, by blanchet
repair invariant in MaSh when learning new proofs
2013-10-18, by blanchet
killed more "no_atp"s
2013-10-18, by blanchet
killed most "no_atp", to make Sledgehammer more complete
2013-10-18, by blanchet
doc fixes suggested by Andreas L.
2013-10-18, by blanchet
make sure that registered code equations are actually equations
2013-10-18, by blanchet
accept very long lines in MaSh
2013-10-18, by blanchet
make sure add: doesn't add duplicates, and works for [no_atp] facts
2013-10-18, by blanchet
no fact subsumption -- this only confuses later code, e.g. 'add:'
2013-10-17, by blanchet
generate a comment storing the goal nickname in "learn_prover"
2013-10-17, by blanchet
clarified message
2013-10-17, by blanchet
added thread-safety warnings
2013-10-17, by blanchet
avoid confusion between outer ifs and inner ifs, that caused tactic to go berserk
2013-10-17, by blanchet
handle nested tuples in 'let's
2013-10-17, by blanchet
more exercises
2013-10-17, by nipkow
also unfold let (_, _) = ... syntax
2013-10-17, by blanchet
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
2013-10-17, by blanchet
graceful handling of abort
2013-10-17, by blanchet
generalized interface
2013-10-17, by panny
choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first
2013-10-17, by blanchet
thread the goal through instead of relying on unreliable (possibly fake) state
2013-10-17, by blanchet
added comment
2013-10-17, by blanchet
tuning
2013-10-17, by blanchet
verbose minimization when learning from ATP proofs
2013-10-17, by blanchet
if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
2013-10-17, by blanchet
if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"
2013-10-17, by blanchet
fast track -- avoid domain error in 0 case
2013-10-17, by blanchet
remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
2013-10-17, by blanchet
merged
2013-10-16, by nipkow
tuned exercises
2013-10-16, by nipkow
use Code.abort instead of undefined in auto-generated equations
2013-10-16, by panny
have MaSh minimize
2013-10-16, by blanchet
tweaked signature
2013-10-15, by blanchet
strengthened tactic to deal with 'False ==> ...'
2013-10-15, by blanchet
made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
2013-10-15, by blanchet
improved duplicate detection in "build_name_tables" by ensuring that the earliest occurrence of a duplicate (if it exists) gets picked as the canonical instance
2013-10-15, by blanchet
updated S/H docs
2013-10-15, by blanchet
use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
2013-10-15, by blanchet
drop only real duplicates, not subsumed facts -- this confuses MaSh
2013-10-15, by blanchet
renamed relcomp_def to relcomp_unfold
2013-10-15, by paulson
fixed thm names
2013-10-15, by nipkow
addressed rare case where the same symbol would be treated alternately as a function and as a predicate -- adding "top2I top_boolI" to a problem that didn't talk about "top" was a way to trigger the issue
2013-10-15, by blanchet
added Nitpick limitations to docs
2013-10-14, by blanchet
more defensive Nitpick setup -- exotic types of recursion are not supported yet in the model finder
2013-10-14, by blanchet
keep temporary error handling in there until code equations are properly generated
2013-10-14, by blanchet
tuning (simplified parts of 92c5bd3b342d)
2013-10-14, by blanchet
tuning
2013-10-14, by blanchet
stengthened tactic to cope with abort cases
2013-10-14, by blanchet
tuned names
2013-10-14, by blanchet
strengthened tactic w.r.t. "let"
2013-10-14, by blanchet
more prominent MaSh errors
2013-10-13, by blanchet
compile -- fix typo introduced in 07a8145aaeba
2013-10-11, by panny
pass the right theorems to tactic
2013-10-11, by panny
prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
2013-10-11, by panny
repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions
2013-10-10, by blanchet
simplify fudge factor code
2013-10-10, by blanchet
cleanup SMT-related config options
2013-10-09, by blanchet
no isar proofs if preplay was not attempted
2013-10-09, by blanchet
normalize more equalities
2013-10-09, by blanchet
parallelize MeSh
2013-10-09, by blanchet
run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
2013-10-09, by blanchet
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
2013-10-09, by blanchet
minor performance tuning
2013-10-09, by blanchet
use plain types instead of dedicated type pattern
2013-10-09, by blanchet
duplicate term and type patterns
2013-10-09, by blanchet
optimized built-in const check
2013-10-09, by blanchet
added TODO
2013-10-09, by blanchet
crank up limit a bit -- truly huge background theories are still nearly 3 times larger
2013-10-09, by blanchet
higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False"
2013-10-08, by blanchet
minor fact filter speedups
2013-10-08, by blanchet
more gracefully handle huge theories in relevance filters
2013-10-08, by blanchet
handle huge MaSh requests gracefully
2013-10-08, by blanchet
further optimization in relevance filter
2013-10-08, by blanchet
further speed up duplicate elimination
2013-10-08, by blanchet
more efficient theorem variable normalization
2013-10-08, by blanchet
strengthened constructor-view tactic to deal with 'let's
2013-10-07, by blanchet
allow 'let's around constructors in constructor view
2013-10-07, by blanchet
reword abstract
2013-10-07, by blanchet
more primcorec docs
2013-10-07, by blanchet
minor doc fix
2013-10-07, by blanchet
new topological lemmas; tuned proofs
2013-10-07, by huffman
strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies)
2013-10-06, by blanchet
generate optimized DNF formula
2013-10-06, by blanchet
rationalized negation code
2013-10-06, by blanchet
honor externally set MASH_PORT
2013-10-05, by blanchet
process code-style inputs
2013-10-04, by panny
more tracing
2013-10-04, by blanchet
more thorough spying
2013-10-04, by blanchet
more Sledgehammer spying -- record fact indices
2013-10-04, by blanchet
prevent explosion in monomorphizer (e.g. when the facts typerep_int_def typerep_num_def typerep_option_def typerep_node_def are selected)
2013-10-04, by blanchet
removed pointless special case
2013-10-04, by blanchet
run fewer provers in "try" mode
2013-10-04, by blanchet
count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)
2013-10-04, by blanchet
more parallelism in blocking mode
2013-10-04, by blanchet
more robustness in MaSh
2013-10-04, by blanchet
back to post-release mode -- after fork point;
2013-10-03, by wenzelm
tuned;
2013-10-03, by wenzelm
tuned;
2013-10-03, by wenzelm
more notes;
2013-10-03, by wenzelm
tuned;
2013-10-03, by wenzelm
added and generalised lemmas
2013-10-03, by nipkow
Streamlined locales reference material.
2013-10-03, by ballarin
merged
2013-10-02, by nipkow
tuned
2013-10-02, by nipkow
merged
2013-10-02, by traytel
keep the qualification of bindings when noting bnf theorems
2013-10-02, by traytel
strengthened tactic (primcorec_sel_tac) + tuning
2013-10-02, by blanchet
renamings
2013-10-02, by blanchet
got rid of needless argument
2013-10-02, by blanchet
make SMT integration slacker w.r.t. bad apples (facts)
2013-10-02, by blanchet
strengthen top sort check
2013-10-02, by blanchet
tuned whitespace;
2013-10-02, by wenzelm
tuned;
2013-10-02, by wenzelm
unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19;
2013-10-02, by wenzelm
updated to scala-2.10.3;
2013-10-02, by wenzelm
tuned;
2013-10-02, by wenzelm
some highlights of Isabelle2013-1 based on NEWS;
2013-10-02, by wenzelm
tuned;
2013-10-02, by wenzelm
misc tuning for release;
2013-10-02, by wenzelm
more (co)data docs
2013-10-02, by blanchet
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
2013-10-02, by blanchet
NEWS and CONTRIBUTORS
2013-10-02, by traytel
made SML/NJ happy
2013-10-02, by traytel
use new coinduction method and primcorec in examples
2013-10-02, by traytel
new coinduction method
2013-10-02, by traytel
tuned command descriptions
2013-10-02, by blanchet
strengthen tactic w.r.t. let
2013-10-02, by blanchet
minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)
2013-10-02, by blanchet
typo
2013-10-02, by kuncar
NEWS and CONTRIBUTORS
2013-10-02, by kuncar
merged
2013-10-01, by blanchet
compile -- broken since 21dac9a60f0c
2013-10-01, by blanchet
strengthened tactic for right-hand sides involving lambdas
2013-10-01, by blanchet
basic documentation for function elimination rules and fun_cases
2013-10-01, by krauss
allow uncurried lambda-abstractions on rhs of "primcorec"
2013-10-01, by blanchet
tiny doc fix
2013-10-01, by blanchet
base the fset bnf on the new FSet theory
2013-10-01, by traytel
improved backwards compatiblity of primrec_new (Isabelle/ML interface, attributes, etc.)
2013-10-01, by traytel
removed spurious save if nothing needs to bee learned
2013-10-01, by blanchet
new version of MaSh that really honors the --port option and that checks for file name mismatches
2013-10-01, by blanchet
minor textual changes
2013-10-01, by blanchet
got rid of dead feature
2013-10-01, by blanchet
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
2013-10-01, by blanchet
renamed ML files
2013-10-01, by blanchet
renamed theory file
2013-10-01, by blanchet
tuned signature -- facilitate experimentation with other processes;
2013-10-01, by wenzelm
preserve types during rewriting
2013-09-30, by Christian Sternagel
made SML/NJ happy
2013-09-30, by blanchet
made SML/NJ happy
2013-09-30, by blanchet
made SML/NJ happier
2013-09-30, by blanchet
added experimental configuration options to tune use of builtin symbols in SMT
2013-09-30, by blanchet