Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
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.
proper qualification needed due to shadowing on theory merge
2010-11-18, by haftmann
more appropriate name for property
2010-11-18, by haftmann
mapper for sum type
2010-11-18, by haftmann
mapper for option type
2010-11-18, by haftmann
mapper for list type; map_pair replaces prod_fun
2010-11-18, by haftmann
map_pair replaces prod_fun
2010-11-18, by haftmann
mapper for mulitset type
2010-11-18, by haftmann
mapper for mapping type
2010-11-18, by haftmann
mapper for fset type
2010-11-18, by haftmann
mapper for dlist type
2010-11-18, by haftmann
map_fun combinator in theory Fun
2010-11-18, by haftmann
some updates after 2 years of Mercurial usage;
2010-11-18, by wenzelm
mention Sledgehammer with SMT
2010-11-18, by blanchet
enabled SMT solver in Sledgehammer by default
2010-11-18, by blanchet
merged
2010-11-18, by haftmann
keep variables bound
2010-11-18, by haftmann
remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
2010-11-18, by blanchet
merged
2010-11-17, by haftmann
infer variances of user-given mapper operation; proper thm storing
2010-11-17, by haftmann
code eqn for slice was missing; redefined splice with fun
2010-11-17, by nipkow
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
2010-11-17, by huffman
merged
2010-11-17, by huffman
typedef (open) unit
2010-11-16, by huffman
add bind_bind rules for powerdomains
2010-11-16, by huffman
merged
2010-11-17, by wenzelm
emerging Isar command interface
2010-11-17, by haftmann
fixed typo
2010-11-17, by haftmann
updated keywords
2010-11-17, by haftmann
ML signature interface
2010-11-17, by haftmann
stub for Isar command interface
2010-11-17, by haftmann
module for functorial mappers
2010-11-17, by haftmann
merged
2010-11-17, by wenzelm
require the b2i file ending in the boogie_open command (for consistency with the theory header)
2010-11-17, by boehmes
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
2010-11-17, by boehmes
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
2010-11-17, by boehmes
add lemmas about powerdomains
2010-11-16, by huffman
declare {upper,lower,convex}_pd_induct as default induction rules
2010-11-16, by huffman
rename 'repdef' to 'domaindef'
2010-11-16, by huffman
refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
2010-11-17, by wenzelm
less parentheses, cf. Session.welcome;
2010-11-17, by wenzelm
avoid spam;
2010-11-16, by wenzelm
more robust determination of java executable;
2010-11-16, by wenzelm
init_component: require absolute path (when invoked by user scripts);
2010-11-16, by wenzelm
more explicit explanation of init_component shell function;
2010-11-16, by wenzelm
paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;
2010-11-16, by wenzelm
tuned message;
2010-11-16, by wenzelm
post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);
2010-11-16, by wenzelm
more reasonably defaults for typical laptops (2 GB RAM, 2 cores);
2010-11-16, by wenzelm
added forall2 predicate lifter
2010-11-16, by haftmann
merged
2010-11-15, by wenzelm
merged
2010-11-15, by boehmes
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
2010-11-15, by boehmes
honour timeouts which are not rounded to full seconds
2010-11-15, by boehmes
better error message
2010-11-15, by blanchet
better error message
2010-11-15, by blanchet
merged
2010-11-15, by wenzelm
cosmetics
2010-11-15, by blanchet
interpret SMT_Failure.Solver_Crashed correctly
2010-11-15, by blanchet
turn on Sledgehammer verbosity so we can track down crashes
2010-11-15, by blanchet
pick up SMT solver crashes and report them to the user/Mirabelle if desired
2010-11-15, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip