Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
tuned proofs
2013-11-19, by blanchet
killed more needless theorems
2013-11-19, by blanchet
killed unused lemmas
2013-11-19, by blanchet
optimized more bad apples
2013-11-19, by blanchet
optimized 'bad apple' method calls
2013-11-19, by blanchet
compile
2013-11-18, by blanchet
no need for 3-way split with GFP for a handful of theorems
2013-11-18, by blanchet
moved more theorems out of LFP
2013-11-18, by blanchet
moved theorems out of LFP
2013-11-18, by blanchet
moved theorems out of LFP
2013-11-18, by blanchet
moved theorems out of LFP
2013-11-18, by blanchet
moved theorems out of LFP
2013-11-18, by blanchet
split 'Cardinal_Arithmetic' 3-way
2013-11-18, by blanchet
started three-way split of 'HOL-Cardinals'
2013-11-18, by blanchet
send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
2013-11-18, by blanchet
merged
2013-11-18, by traytel
show all involved subtyping constraints that cause coercion inference to fail
2013-11-18, by traytel
additional lemmas in BNF/Examples/Stream
2013-11-18, by hoelzl
reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798
2013-11-18, by traytel
comments by Sean Seefried
2013-11-18, by nipkow
more robust example;
2013-11-17, by wenzelm
tuned proofs;
2013-11-17, by wenzelm
tuned;
2013-11-17, by wenzelm
tuned proofs;
2013-11-17, by wenzelm
explicit indication of thy_load commands;
2013-11-17, by wenzelm
centralized management of pending buffer edits;
2013-11-17, by wenzelm
merged
2013-11-17, by nipkow
added functions all and exists to IArray
2013-11-16, by nipkow
prefer explicit "document" flag -- eliminated stateful Present.no_document;
2013-11-16, by wenzelm
simplified HTML linefeed (again, see 041dc6d8d344);
2013-11-16, by wenzelm
simplified HTML theory presentation;
2013-11-16, by wenzelm
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
2013-11-16, by wenzelm
tuned;
2013-11-16, by wenzelm
merged
2013-11-16, by wenzelm
tuned proofs;
2013-11-16, by wenzelm
tuned signature;
2013-11-16, by wenzelm
tuned signature -- clarified Proof General legacy;
2013-11-16, by wenzelm
toplevel function "use" refers to raw ML bootstrap environment;
2013-11-16, by wenzelm
obsolete;
2013-11-16, by wenzelm
proper thy_load command 'boogie_file' -- avoid direct access to file-system;
2013-11-16, by wenzelm
tuned signature;
2013-11-16, by wenzelm
updated example;
2013-11-16, by wenzelm
prefer UTF8.decode_permissive;
2013-11-16, by wenzelm
more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;
2013-11-16, by wenzelm
more specific Protocol_Output: empty message.body, main content via bytes/text;
2013-11-15, by wenzelm
tuned imports;
2013-11-14, by wenzelm
tuned signature;
2013-11-14, by wenzelm
immutable byte vectors versus UTF8 strings;
2013-11-14, by wenzelm
dropped duplicate of of_bool
2013-11-15, by haftmann
proper code equations for Gcd and Lcm on nat and int
2013-11-15, by haftmann
tuned
2013-11-16, by nipkow
fixed type variable confusion in 'datatype_new_compat'
2013-11-14, by blanchet
implemented 'tptp_translate'
2013-11-14, by blanchet
reintroduced (unimplemented) 'tptp_translate' tool
2013-11-14, by blanchet
have MaSh support nameless facts (i.e. proofs) and use that support
2013-11-14, by blanchet
made SML/NJ happy
2013-11-14, by blanchet
renamed thm
2013-11-14, by blanchet
explicit inclusion of data refinement theory into HOL-Library session
2013-11-14, by haftmann
tuned to improve automation (for REPEAT)
2013-11-14, by nipkow
separated comparision on bit operations into separate theory
2013-11-13, by haftmann
prohibit locally fixed type variables in bnf definitions
2013-11-13, by traytel
tuned
2013-11-13, by traytel
standard relator for list bnf
2013-11-13, by traytel
tuned example
2013-11-13, by traytel
shortened generated property name
2013-11-13, by blanchet
more explicit syntax for defining a bnf
2013-11-13, by traytel
fix document generation for HOL-Probability
2013-11-13, by hoelzl
fix document generation for Extended_Nat
2013-11-12, by hoelzl
measure of a countable union
2013-11-12, by hoelzl
add restrict_space measure
2013-11-12, by hoelzl
better support for enat and ereal conversions
2013-11-12, by hoelzl
enat is countable
2013-11-12, by hoelzl
add equalities for SUP and INF over constant functions
2013-11-12, by hoelzl
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
2013-11-12, by hoelzl
add acyclicI_order
2013-11-12, by hoelzl
stronger inc_induct and dec_induct
2013-11-12, by hoelzl
countability of the image of a reflexive transitive closure
2013-11-12, by hoelzl
support of_rat with 0 or 1 on order relations
2013-11-12, by hoelzl
equation when indicator function equals 0 or 1
2013-11-12, by hoelzl
ported part of function package to new 'Ctr_Sugar' abstraction
2013-11-12, by blanchet
undid copy-paste
2013-11-12, by blanchet
ported 'partial_function' to 'Ctr_Sugar' abstraction
2013-11-12, by blanchet
port list comprehension simproc to 'Ctr_Sugar' abstraction
2013-11-12, by blanchet
added convenience function
2013-11-12, by blanchet
document idiomatic use of 'simps_of_case'
2013-11-12, by blanchet
ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction
2013-11-12, by blanchet
register old-style datatypes as 'Ctr_Sugar'
2013-11-12, by blanchet
export useful ML function
2013-11-12, by blanchet
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
2013-11-12, by blanchet
tuned headers
2013-11-12, by blanchet
moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction
2013-11-12, by blanchet
updated sessions;
2013-11-12, by wenzelm
proper latex -- NB: cannot use antiquotation here;
2013-11-12, by wenzelm
merged
2013-11-11, by wenzelm
simplified App template;
2013-11-11, by wenzelm
obsolete;
2013-11-11, by wenzelm
obsolete;
2013-11-11, by wenzelm
tuned message;
2013-11-11, by wenzelm
tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
2013-11-11, by wenzelm
tuned signature;
2013-11-11, by wenzelm
minor doc fix
2013-11-11, by blanchet
merged
2013-11-11, by wenzelm
merged, using src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML and src/HOL/Tools/Sledgehammer/sledgehammer_run.ML from 347c3b0cab44;
2013-11-11, by wenzelm
removed obsolete RC tags;
2013-11-11, by wenzelm
Added tag Isabelle2013-1 for changeset 9c1f21365326
2013-11-11, by wenzelm
tuned;
Isabelle2013-1
2013-11-09, by wenzelm
more on completion;
2013-11-09, by wenzelm
adjust modules for Admin/build jars_test;
2013-11-09, by wenzelm
tuned whitespace;
2013-11-09, by wenzelm
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
2013-11-08, by wenzelm
transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
2013-11-08, by wenzelm
Added tag Isabelle2013-1-RC4 for changeset 594628261376
2013-11-07, by wenzelm
updated to polyml-5.5.1-1 (fixes-5.5.1 version 1875);
2013-11-07, by wenzelm
tuned;
2013-11-07, by wenzelm
misc tuning;
2013-11-07, by wenzelm
updated to jedit_build-20131106 (Console.jar 5.1.3);
2013-11-06, by wenzelm
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
2013-11-06, by wenzelm
tuned signature;
2013-11-06, by wenzelm
less tiny font for search criteria;
2013-11-06, by wenzelm
tuned tooltips;
2013-11-06, by wenzelm
swap equations and premises in the coinductive step for better proof automation
2013-10-17, by Andreas Lochbihler
no default shortcut for isabelle.reset-font-size -- avoid conflict with unsplit-current;
2013-11-05, by wenzelm
tuned;
2013-11-05, by wenzelm
CONTRIBUTORS
2013-10-28, by noschinl
more on text completion;
2013-11-03, by wenzelm
tuned;
2013-11-03, by wenzelm
more on Monitor panel;
2013-11-03, by wenzelm
more on Timing;
2013-11-03, by wenzelm
more on miscellaneous tools;
2013-11-01, by wenzelm
more screenshots;
2013-10-31, by wenzelm
more screenshots;
2013-10-31, by wenzelm
more on Sledgehammer;
2013-10-31, by wenzelm
more on automatically tried tools;
2013-10-31, by wenzelm
more on prover output;
2013-10-30, by wenzelm
misc tuning and clarification;
2013-10-30, by wenzelm
more on file-system access;
2013-10-30, by wenzelm
tuned;
2013-10-29, by wenzelm
more on problems and workarounds;
2013-10-29, by wenzelm
tuned;
2013-10-29, by wenzelm
clarified isabelle options -l;
2013-10-29, by wenzelm
tuned;
2013-10-29, by wenzelm
clarified workaround: problem is potential blocking of vacuous input (see also Poly/ML SVN 1874);
2013-10-16, by wenzelm
removed dead code (see also db4bf4fb5492);
2013-10-14, by wenzelm
Added tag Isabelle2013-1-RC3 for changeset fbcaa9f08879
2013-10-16, by wenzelm
avoid non-portable int constant -- make SML/NJ happy;
2013-10-16, by wenzelm
avoid empty input and its adverse effect on socket communication, e.g. output message getting "stuck" after vacuous update due to Session.update_options;
2013-10-16, by wenzelm
prefer TCP_NODELAY -- avoid extra buffering due to Nagle's algorithm;
2013-10-16, by wenzelm
basic IO buffer size like for fifo -- imitate implicit flushing behaviour more closely;
2013-10-16, by wenzelm
removed junk (cf. 409d7f7247f4);
2013-10-14, by wenzelm
fix a citation
2013-10-14, by kuncar
declare Quotient_Examples/FSet.thy as almost obsolete
2013-10-14, by kuncar
update documentation of important public ML functions in Lifting
2013-10-14, by kuncar
update documentation of Lifting/Transfer and Quotient
2013-10-14, by kuncar
don't allow parametricity theorem for typedefs in setup_lifting. The theorem is not used.
2013-10-11, by kuncar
tuned;
2013-10-14, by wenzelm
more screenshots;
2013-10-12, by wenzelm
tuned;
2013-10-12, by wenzelm
misc tuning;
2013-10-12, by wenzelm
more strict find_command -- avoid invalid hyperlink_command;
2013-10-12, by wenzelm
more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;
2013-10-11, by wenzelm
obsolete;
2013-10-11, by wenzelm
clarified Editor.current_command: allow outdated snapshot;
2013-10-11, by wenzelm
make double sure that AWT/Swing antialiasing is enabled (see also http://www.jedit.org/users-guide/jvm-options.html and jdk/src/share/classes/sun/awt/SunToolkit.java);
2013-10-11, by wenzelm
more documentation;
2013-10-10, by wenzelm
more documentation;
2013-10-10, by wenzelm
more documentation;
2013-10-10, by wenzelm
tuned;
2013-10-10, by wenzelm
NEWS;
2013-10-09, by wenzelm
avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus);
2013-10-09, by wenzelm
add congruence rule to prevent code_simp from looping
2013-10-09, by Andreas Lochbihler
Added tag Isabelle2013-1-RC2 for changeset 782e430e6a83
2013-10-09, by wenzelm
native executable for Linux (see Admin/Linux);
2013-10-07, by wenzelm
proper NULL termination;
2013-10-07, by wenzelm
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
2013-10-07, by wenzelm
proper warning at run time, not in the parser;
2013-10-07, by wenzelm
prefer "fresh" open -- requires Lion / Mountain Lion;
2013-10-07, by wenzelm
clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
2013-10-07, by wenzelm
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
more parallelism in blocking 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
another shortcut alias;
2013-10-04, by wenzelm
NEWS;
2013-10-04, by wenzelm
Added tag Isabelle2013-1-RC1 for changeset c37100233af7
2013-10-03, by wenzelm
reintroduced check from bd36da55d825 after all, due to hard-to-solve issues outside the N2M code
2013-11-11, by blanchet
removed dead code
2013-11-11, by blanchet
added check to avoid odd situations the N2M code cannot handle
2013-11-11, by blanchet
reverted check introduced in ce58fb149ff6, now that independent functions are allowed (cf. 347c3b0cab44)
2013-11-11, by blanchet
tuned signature
2013-11-11, by blanchet
handle independent functions defined in parallel in N2M (in presence of type variables, see ce58fb149ff6)
2013-11-11, by traytel
tuned
2013-11-11, by nipkow
tuned
2013-11-11, by nipkow
qualifed popular user space names
2013-11-10, by haftmann
dropped obsolete check: dest_num always yields positive number
2013-11-10, by haftmann
simplified: negative number is trivially smaller than 2, and SMT_Builtin.is_builtin_num implies that its argument is a number
2013-11-10, by haftmann
more exercises
2013-11-08, by nipkow
by (auto ...)[1] not by (auto [1])
2013-11-08, by blanchet
added exercise
2013-11-08, by nipkow
Add output translation for <a := .., b := .., ..> state notation.
2013-11-07, by kleing
reintroduce mutually (co)rec check, since the underlying N2M code doesn't quite handle the general case (esp. in presence of type variables)
2013-11-07, by blanchet
more docs
2013-11-07, by blanchet
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
2013-11-07, by blanchet
reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP
2013-11-06, by blanchet
simplified code
2013-11-06, by blanchet
fourth attempt at generalizing N2M types (to leverage caching)
2013-11-06, by blanchet
tuning
2013-11-06, by blanchet
int and nat are conditionally_complete_lattices
2013-11-05, by hoelzl
be more open-minded and allow needless mutual recursion for 'prim(co)rec', since we allow it for '(co)datatype' -- eventual warnings (or errors) should be centralized in 'fp_bnf'
2013-11-06, by blanchet
removed dead code
2013-11-06, by blanchet
update docs
2013-11-06, by blanchet
take out possibility of moving corecursive calls past constructors -- this doesn't work in the general case
2013-11-06, by blanchet
took out loopy code
2013-11-06, by blanchet
take out even less aggressive generalization -- it's still too aggressive
2013-11-06, by blanchet
reverted too aggressive 7cb8442298f0
2013-11-06, by blanchet
generalize more aggressively
2013-11-06, by blanchet
avoid subtle failure in the presence of top sort
2013-11-05, by blanchet
tuning
2013-11-05, by blanchet
get mutually recursive maps as well
2013-11-05, by blanchet
tuned proofs in Approximation
2013-11-05, by hoelzl
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip