isabelle: Graph

fixed subtle name shadowing bug
2013-11-05, by blanchet
use right permutation in 'map2'
2013-11-05, by blanchet
stronger normalization, to increase n2m cache effectiveness
2013-11-05, by blanchet
make local theory operations non-pervasive (makes more intuitive sense)
2013-11-05, by blanchet
NEWS
2013-11-05, by hoelzl
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-05, by hoelzl
generalize bdd_above/below_uminus to ordered_ab_group_add
2013-11-05, by hoelzl
restrict Limsup and Liminf to complete lattices
2013-11-05, by hoelzl
use INF and SUP on conditionally complete lattices in multivariate analysis
2013-11-05, by hoelzl
add SUP and INF for conditionally complete lattices
2013-11-05, by hoelzl
use bdd_above and bdd_below for conditionally complete lattices
2013-11-05, by hoelzl
generalize SUP and INF to the syntactic type classes Sup and Inf
2013-11-05, by hoelzl
added some N2M caching
2013-11-05, by blanchet
also generalize fixed types
2013-11-05, by blanchet
generalize types when synthetizing n2m (co)recursors, to facilitate reuse
2013-11-05, by blanchet
nicer error message in case of duplicates
2013-11-05, by blanchet
use int example like in the rest of IMP (instead of nat)
2013-11-05, by kleing
dropped dead code
2013-11-04, by haftmann
fact generalization and name consolidation
2013-11-04, by haftmann
streamlined setup of linear arithmetic
2013-11-04, by haftmann
make 'try0' return faster when invoked as part of 'try'
2013-11-04, by blanchet
careful with lists of different lengths
2013-11-04, by blanchet
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
2013-11-04, by blanchet
better error handling
2013-11-04, by blanchet
more robust treatment of dead variables in n2m
2013-11-04, by traytel
more robust n2m w.r.t. 'let's
2013-11-04, by blanchet
tuning
2013-11-04, by blanchet
strengthened tactic
2013-11-04, by blanchet
made n2m code more robust w.r.t. advanced constructs (e.g. lambdas)
2013-11-04, by blanchet
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
added possibility to reset builtins (for experimentation)
2013-09-30, by blanchet
just one data slot (record) per program unit
2013-09-30, by blanchet
more "primrec_new" documentation
2013-09-30, by blanchet
merged
2013-09-30, by wenzelm
tuned signature;
2013-09-30, by wenzelm
eliminated clone of Inductive.mk_cases_tac;
2013-09-30, by wenzelm
tuned signature;
2013-09-30, by wenzelm
tuned whitespace;
2013-09-30, by wenzelm
provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);
2013-09-30, by wenzelm
merge
2013-09-30, by blanchet
minor tweak to error message
2013-09-30, by blanchet
tuned;
2013-09-30, by wenzelm
explicit caret position after replacement;
2013-09-29, by wenzelm
tuned proofs
2013-09-29, by haftmann
observe user preferences;
2013-09-29, by wenzelm
updated for release;
2013-09-29, by wenzelm
tuned;
2013-09-29, by wenzelm
tuned;
2013-09-29, by wenzelm
more on text completion;
2013-09-29, by wenzelm
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
2013-09-29, by wenzelm
updated for release;
2013-09-29, by wenzelm
updated for release;
2013-09-29, by wenzelm
updated to sumatra_pdf-2.3.2;
2013-09-29, by wenzelm
low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;
2013-09-29, by wenzelm
backout c6297fa1031a -- strange parsers are required to make this work;
2013-09-29, by wenzelm
make SML/NJ more happy;
2013-09-28, by wenzelm
enforce IsabelleText font for better symbol coverage, especially on Windows;
2013-09-28, by wenzelm
proper wrapper for parser -- more explicit error;
2013-09-28, by wenzelm
misc tuning for release;
2013-09-28, by wenzelm
remove remains from WinRun4J;
2013-09-28, by wenzelm
proper document markup;
2013-09-28, by wenzelm
uniform $ISABELLE_HOME on all platforms;
2013-09-28, by wenzelm
simplified ISABELLE_HOME on Windows (see also 9c8a1b9c0630, 5a7903ba2dac);
2013-09-28, by wenzelm
update second environment that is used for System.getenv(String);
2013-09-28, by wenzelm
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
2013-09-28, by wenzelm
tuned names
2013-09-27, by kuncar
fold and lemmas about cardinality
2013-09-27, by kuncar
more robust parser: 'imports' are mandatory except for bootstrapping Pure;
2013-09-27, by wenzelm
one more unfolding necessary
2013-09-27, by blanchet
faster exit in common case
2013-09-27, by blanchet
merged
2013-09-27, by nipkow
hide coercion
2013-09-27, by nipkow
fixed one line that would never have compiled in a typed language + release the lock in case of exceptions
2013-09-27, by blanchet
merged
2013-09-27, by nipkow
added Bleast code eqns for RBT
2013-09-27, by nipkow
added code eqns for bounded LEAST operator
2013-09-27, by nipkow
new theory of finite sets as a subtype
2013-09-27, by kuncar
new parametricity rules and useful lemmas
2013-09-27, by kuncar
allow to specify multiple parametricity transfer rules in lift_definition
2013-09-27, by kuncar
merged
2013-09-27, by Andreas Lochbihler
generalise lemma
2013-09-27, by Andreas Lochbihler
proper latex;
2013-09-27, by wenzelm
merged
2013-09-27, by Andreas Lochbihler
add relator for 'a filter and parametricity theorems
2013-09-27, by Andreas Lochbihler
tuned proofs
2013-09-27, by Andreas Lochbihler
add lemmas
2013-09-27, by Andreas Lochbihler
prefer Code.abort over code_abort
2013-09-27, by Andreas Lochbihler
merged
2013-09-27, by lammich
Added Item_Net.retrieve_matching
2013-09-26, by lammich
Added symmetric code_unfold-lemmas for null and is_none
2013-09-26, by lammich
tuned proofs
2013-09-26, by huffman
moved lemma
2013-09-26, by huffman
merged
2013-09-26, by wenzelm
proper regexp;
2013-09-26, by wenzelm
added Isabelle/ML example;
2013-09-26, by wenzelm
updated jedit.jar, jEdit-patched.tar.gz according to 239f8f451976;
2013-09-26, by wenzelm
workaround for action-bar shortcut on Mac OS X L&F: avoid EnhancedMenuItem.setAccelerator which causes conflict with regular key handling and thus double invocation -- see also jEdit.actionContext (if actionBarVisible view.removeToolBar);
2013-09-26, by wenzelm
more uniform modes (NB: comments etc. are handled by isabelle.Token_Markup.Marker);
2013-09-26, by wenzelm
support more brackets (see also 427724cff970, 7bf637b65ba2);
2013-09-26, by wenzelm
tuned proofs
2013-09-26, by huffman
further strengthening of tactics
2013-09-26, by blanchet
merged
2013-09-26, by Andreas Lochbihler
add lemmas
2013-09-26, by Andreas Lochbihler
strengthened tactic
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
avoid calls to nth with ~1
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
strengthened tactic
2013-09-26, by blanchet
tactic cleanup
2013-09-26, by blanchet
made tactic more robust in case somebody specified a discriminator for a one-constructor type
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
use new "sel_split(_asm)" to avoid giving rise to quantifiers, which would in turn require relying on injectivity
2013-09-26, by blanchet
generate "sel_splits(_asm)" theorems
2013-09-26, by blanchet
generate "sel_exhaust" theorem
2013-09-26, by blanchet
merged
2013-09-26, by wenzelm
obsolete (see also 48d13465c7c7);
2013-09-26, by wenzelm
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
2013-09-26, by wenzelm
initialize class immediately (potentially more robust);
2013-09-26, by wenzelm
tuned
2013-09-26, by nipkow
strengthen tactic
2013-09-26, by blanchet
use needed case theorems
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
added data query function
2013-09-26, by blanchet
added data query function
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
got rid of dependency on silly 'eq_ifI' theorem
2013-09-26, by blanchet
more powerful/robust tactics
2013-09-26, by blanchet
use standard "split" properties instead of ad hoc "eq_...I"
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
made tactic more flexible w.r.t. case expressions and such
2013-09-26, by blanchet
simplified code
2013-09-25, by panny
simplified directory structure;
2013-09-25, by wenzelm
obsolete (see da57c4912987);
2013-09-25, by wenzelm
don't generate wrong type
2013-09-25, by blanchet
proper handling of abstractions
2013-09-25, by blanchet
fixed off-by-one bug
2013-09-25, by blanchet
further improved 'code' helper functions
2013-09-25, by blanchet
removed spurious recursion
2013-09-25, by blanchet
robustness
2013-09-25, by blanchet
thread through bound types
2013-09-25, by blanchet
killed redundant argument
2013-09-25, by blanchet
improved massaging of case expressions
2013-09-25, by blanchet
filled in gap in library offering
2013-09-25, by blanchet
updated documentation concerning MacOSX plugin 1.3;
2013-09-25, by wenzelm
merged
2013-09-25, by wenzelm
bypass Isabelle OSX_Adapter for now -- MacOSX plugin 1.3 manages that better;
2013-09-25, by wenzelm
include MacOSX plugin by default -- disabled by default to avoid multiplatform confusion;
2013-09-25, by wenzelm
removed obsolete cobra.jar, js.jar (see also 30de372ca56f);
2013-09-25, by wenzelm
merged
2013-09-25, by nipkow
tuned
2013-09-25, by nipkow
break more conjunctions
2013-09-25, by blanchet
move useful functions to library
2013-09-25, by blanchet
merge
2013-09-25, by panny
simplified code
2013-09-25, by panny
add non-corecursive constructor view theorems to simps
2013-09-25, by panny
merged
2013-09-25, by wenzelm
tuned proofs;
2013-09-25, by wenzelm
explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
2013-09-25, by wenzelm
more powerful fold
2013-09-25, by blanchet
properly fold over branches
2013-09-25, by blanchet
tuned
2013-09-25, by nipkow
removed dead code
2013-09-25, by blanchet
keep a database of free constructor type information
2013-09-25, by blanchet
generalized case-handling code a bit
2013-09-25, by blanchet
support cases for new-style (co)datatypes
2013-09-25, by blanchet
use case rather than sequence of ifs in expansion
2013-09-25, by blanchet
textual improvements following Christian Sternagel's feedback
2013-09-25, by blanchet
generalize lemma
2013-09-24, by huffman
removed unused lemma
2013-09-24, by huffman
factor out new lemma
2013-09-24, by huffman
replace lemma with more general simp rule
2013-09-24, by huffman
generalized tactics
2013-09-24, by blanchet
renamed generated property
2013-09-24, by blanchet
commented out debugging output in "primcorec"
2013-09-24, by blanchet
merged
2013-09-24, by wenzelm
tuned proofs;
2013-09-24, by wenzelm
more quasi-generic PIDE modules (NB: Swing/JFX needs to be kept separate from non-GUI material);
2013-09-24, by wenzelm
NEWS;
2013-09-24, by wenzelm
clarified font;
2013-09-24, by wenzelm
simplified default L&F -- Nimbus should be always available and GTK+ is not fully working yet;
2013-09-24, by wenzelm
proper platform-specific test;
2013-09-24, by wenzelm
disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;
2013-09-24, by wenzelm
focus text field, to capture key events even on Mac OS X look-and-feel;
2013-09-24, by wenzelm
tuned proofs;
2013-09-24, by wenzelm
more tolerant treatment of end-of-buffer -- avoid debatable situations of jEdit buffer boundaries;
2013-09-24, by wenzelm
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
2013-09-24, by wenzelm
clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer);
2013-09-24, by wenzelm
tuned proofs;
2013-09-24, by wenzelm
obsolete;
2013-09-24, by wenzelm
tuned;
2013-09-24, by wenzelm
avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);
2013-09-24, by wenzelm
tuned isatest options;
2013-09-24, by wenzelm
updated docs
2013-09-24, by blanchet
added [dest] to "disc_exclude"
2013-09-24, by blanchet
started adding support for "nat_case" as case study for all "case" constructs
2013-09-24, by blanchet
temporary fix to tactic
2013-09-24, by blanchet
made SML/NJ happy
2013-09-24, by blanchet
tuning
2013-09-24, by blanchet
support "of" syntax to disambiguate selector equations
2013-09-24, by panny
don't note more induction principles than there are functions + tuning
2013-09-24, by blanchet
more (co)data docs
2013-09-24, by blanchet
improved rail diagram
2013-09-24, by blanchet
use "primcorec" in example
2013-09-24, by blanchet
use "primcorec" in doc
2013-09-24, by blanchet
updated keywords
2013-09-24, by blanchet
updated certificates
2013-09-24, by blanchet
when "max_thm_instances" is hit, choose more carefully which instances should be kept
2013-09-24, by blanchet
add "primcorec" command (cf. ae7f50e70c09)
2013-09-24, by panny
merged
2013-09-24, by nipkow
added lemmas
2013-09-24, by nipkow
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
2013-09-24, by blanchet
adapted to reflect renaming of session
2013-09-24, by blanchet
merged
2013-09-24, by Andreas Lochbihler
make measure_of total
2013-09-24, by Andreas Lochbihler
encode goal digest in spying log (to detect duplicates)
2013-09-24, by blanchet
made SML/NJ happy
2013-09-24, by blanchet
tuned proofs
2013-09-23, by huffman
use forthcoming "primcorec" command
2013-09-24, by blanchet
set code and nitpick_simp attributes on primcorec theorems
2013-09-24, by blanchet
tuning
2013-09-24, by blanchet
tuned docs
2013-09-24, by blanchet
register codatatypes with Nitpick
2013-09-24, by blanchet
register codatatypes with Nitpick
2013-09-23, by blanchet
don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)
2013-09-23, by blanchet
added [code] to selectors
2013-09-23, by blanchet
tuned spying
2013-09-23, by blanchet
document "spy"
2013-09-23, by blanchet
added "spy" option to Nitpick
2013-09-23, by blanchet
document "spy" option
2013-09-23, by blanchet
added "spy" option to Sledgehammer
2013-09-23, by blanchet
proper text for document preparation;
2013-09-23, by wenzelm
set [code] on case equations
2013-09-23, by blanchet
note coinduct theorems in "primcorec"
2013-09-23, by blanchet
tuning
2013-09-23, by blanchet
generate "simps" from "primcorec"
2013-09-23, by blanchet
undid copy-paste
2013-09-23, by blanchet
avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code)
2013-09-23, by blanchet
don't generate empty theorem collections
2013-09-23, by blanchet
tuned code
2013-09-23, by blanchet
provide a way to override MaSh's port from configuration file
2013-09-23, by blanchet
new version of MaSh program, with proper shutdown
2013-09-23, by blanchet