isabelle: Graph

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
merged
2010-11-15, by boehmes
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
2010-11-15, by boehmes
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
2010-11-15, by boehmes
merged
2010-11-15, by bulwahn
ignoring the constant STR in the predicate compiler
2010-11-15, by bulwahn
non-executable source files;
2010-11-15, by wenzelm
eliminated old-style sed in favour of builtin regex matching;
2010-11-15, by wenzelm
more robust treatment of spaces in file names;
2010-11-15, by wenzelm
tuned error messages;
2010-11-15, by wenzelm
merged
2010-11-15, by wenzelm
re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
2010-11-15, by haftmann
re-generalized type of prod_rel (accident from 2989f9f3aa10)
2010-11-15, by haftmann
formal dependency on b2i files
2010-11-15, by boehmes
merged
2010-11-14, by boehmes
check the return code of the SMT solver and raise an exception if the prover failed
2010-11-12, by boehmes
updated README;
2010-11-14, by wenzelm
tuned;
2010-11-14, by wenzelm
cover 'write' as primitive proof command;
2010-11-14, by wenzelm
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
2010-11-14, by wenzelm
somewhat adhoc replacement for 'thus' and 'hence';
2010-11-13, by wenzelm
always print state of proof commands (notably "qed" etc.);
2010-11-13, by wenzelm
simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
2010-11-13, by wenzelm
tuned message;
2010-11-13, by wenzelm
proper escape in regex;
2010-11-13, by wenzelm
report malformed symbols;
2010-11-13, by wenzelm
qualified Symbol_Pos.symbol;
2010-11-13, by wenzelm
total Symbol.source;
2010-11-13, by wenzelm
eliminated slightly odd pervasive Symbol_Pos.symbol;
2010-11-13, by wenzelm
treat Unicode "replacement character" (i.e. decoding error) is malformed;
2010-11-13, by wenzelm
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
2010-11-13, by wenzelm
tuned;
2010-11-13, by wenzelm
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
2010-11-13, by wenzelm
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
2010-11-13, by wenzelm
updated README;
2010-11-13, by wenzelm
defensive defaults for more robust experience for new users;
2010-11-12, by wenzelm
merged
2010-11-12, by wenzelm
preliminary support for newer versions of Z3
2010-11-12, by boehmes
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
2010-11-12, by boehmes
let the theory formally depend on the Boogie output
2010-11-12, by boehmes
look for certificates relative to the theory
2010-11-12, by boehmes
dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT
2010-11-12, by boehmes
merged
2010-11-12, by huffman
update Theory.requires with new theory name
2010-11-12, by huffman
tuned signatures;
2010-11-12, by wenzelm
never open Unsynchronized;
2010-11-12, by wenzelm
merged
2010-11-12, by wenzelm
section headings
2010-11-10, by huffman
reorder chapters for generated document
2010-11-10, by huffman
merge Representable.thy into Domain.thy
2010-11-10, by huffman
move stuff from Domain.thy to Domain_Aux.thy
2010-11-10, by huffman
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
2010-11-10, by huffman
allow unpointed lazy arguments for definitional domain package
2010-11-10, by huffman
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
2010-11-10, by huffman
merged
2010-11-10, by huffman
removed unused lemma chain_mono2
2010-11-10, by huffman
rename class 'bifinite' to 'domain'
2010-11-10, by huffman
instance sum :: (predomain, predomain) predomain
2010-11-10, by huffman
configure sum type for fixrec
2010-11-10, by huffman
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
2010-11-10, by huffman
instance prod :: (predomain, predomain) predomain
2010-11-10, by huffman
adapt isodefl proof script to unpointed types
2010-11-09, by huffman
add 'predomain' class: unpointed version of bifinite
2010-11-09, by huffman
add bifiniteness check for domain_isomorphism command
2010-11-09, by huffman
implement map_of_typ using Pattern.rewrite_term
2010-11-09, by huffman
avoid using stale theory
2010-11-09, by huffman
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
2010-11-08, by huffman
add function the_sort
2010-11-08, by huffman
refactor tmp_thy code
2010-11-08, by huffman
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
2010-11-08, by huffman
treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
2010-11-12, by wenzelm
Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;
2010-11-12, by wenzelm
more precise treatment of deleted nodes;
2010-11-11, by wenzelm
tuned error message;
2010-11-11, by wenzelm
unified type Document.Edit;
2010-11-11, by wenzelm
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
2010-11-11, by wenzelm
tuned;
2010-11-11, by wenzelm
reduced danger of line breaks within minipage;
2010-11-11, by wenzelm
Sidekick block asset: show first line only;
2010-11-10, by wenzelm
added buffer_text convenience, with explicit locking;
2010-11-10, by wenzelm
use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading);
2010-11-10, by wenzelm
merged
2010-11-10, by wenzelm
make SML/NJ happy
2010-11-10, by blanchet
merged
2010-11-09, by haftmann
slightly changed fun_map_def
2010-11-09, by haftmann
fun_rel_def is no simp rule by default
2010-11-09, by haftmann
more appropriate specification packages; fun_rel_def is no simp rule by default
2010-11-09, by haftmann
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
2010-11-09, by haftmann
more appropriate specification packages; fun_rel_def is no simp rule by default
2010-11-09, by haftmann
type annotations in specifications; fun_rel_def is no simp rule by default
2010-11-09, by haftmann
fun_rel_def is no simp rule by default
2010-11-09, by haftmann
merged
2010-11-09, by paulson
tidied using metis
2010-11-09, by paulson
manage folding via sidekick by default;
2010-11-10, by wenzelm
eliminated obsolete heading category -- superseded by heading_level;
2010-11-10, by wenzelm
treat main theory commands like headings, and nest anything else inside;
2010-11-10, by wenzelm
proper treatment of equal heading level;
2010-11-10, by wenzelm
added missing Keyword.THY_SCHEMATIC_GOAL;
2010-11-10, by wenzelm
default Sidekick parser based on section headings;
2010-11-10, by wenzelm
some support for nested source structure, based on section headings;
2010-11-10, by wenzelm
tuned;
2010-11-10, by wenzelm
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
2010-11-09, by wenzelm
updated version;
2010-11-09, by wenzelm
private counter, to keep externalized ids a bit smaller;
2010-11-09, by wenzelm
added general Synchronized.counter convenience;
2010-11-09, by wenzelm
explicitly identify forked/joined tasks;
2010-11-09, by wenzelm
accomodate old manuals that include pdfsetup.sty without isabelle.sty;
2010-11-09, by wenzelm
merged
2010-11-09, by wenzelm
removed type-inference-like behaviour from relation_tac completely; tuned
2010-11-08, by krauss
avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
2010-11-08, by wenzelm
explicitly check uniqueness of symbol recoding;
2010-11-08, by wenzelm
more hints on building and running Isabelle/jEdit from command line;
2010-11-08, by wenzelm
merged
2010-11-08, by wenzelm
merge
2010-11-08, by blanchet
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
2010-11-08, by blanchet
merged
2010-11-08, by huffman
merged
2010-11-06, by huffman
(infixl "<<" 55) -> (infix "<<" 50)
2010-11-05, by huffman
simplify some proofs
2010-11-03, by huffman
remove unnecessary stuff from Discrete.thy
2010-11-03, by huffman
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
2010-11-03, by huffman
add lemma eq_imp_below
2010-11-03, by huffman
discontinue a bunch of legacy theorem names
2010-11-03, by huffman
move a few admissibility lemmas into FOCUS/Stream_adm.thy
2010-11-03, by huffman
simplify some proofs
2010-11-03, by huffman
compile -- 7550b2cba1cb broke the build
2010-11-08, by blanchet
merge
2010-11-08, by blanchet
recognize Vampire error
2010-11-08, by blanchet
return the process return code along with the process outputs
2010-11-08, by boehmes
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-11-08, by boehmes
merged
2010-11-08, by haftmann
corrected slip: must keep constant map, not type map; tuned code
2010-11-08, by haftmann
constructors to datatypes in code_reflect can be globbed; dropped unused code
2010-11-08, by haftmann
adding code and theory for smallvalue generators, but do not setup the interpretation yet
2010-11-08, by bulwahn
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
2010-11-08, by blanchet
better detection of completely irrelevant facts
2010-11-08, by blanchet
always use a hard timeout in Mirabelle
2010-11-07, by blanchet
use "smt" (rather than "metis") to reconstruct SMT proofs
2010-11-07, by blanchet
don't pass too many facts on the first iteration of the SMT solver
2010-11-07, by blanchet
catch TimeOut exception
2010-11-07, by blanchet
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
2010-11-07, by blanchet
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
2010-11-07, by blanchet
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
2010-11-07, by blanchet
make Nitpick datatype tests faster to make timeout less likely
2010-11-06, by blanchet
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
2010-11-06, by blanchet
always honor the max relevant constraint
2010-11-06, by blanchet
more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;
2010-11-08, by wenzelm
updated generated files;
2010-11-08, by wenzelm
tweaked pdf setup to allow modification of \pdfminorversion;
2010-11-07, by wenzelm
merged;
2010-11-07, by wenzelm
updated generated files;
2010-11-07, by wenzelm
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
2010-11-07, by wenzelm
updated generated file;
2010-11-07, by wenzelm
more literal appearance of antiqopen/antiqclose;
2010-11-07, by wenzelm
'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
2010-11-07, by wenzelm
continue after failed commands;
2010-11-06, by wenzelm
added Keyword.is_heading (cf. Scala version);
2010-11-06, by wenzelm
updated keywords;
2010-11-06, by wenzelm
mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
2010-11-06, by wenzelm
somewhat more uniform timing markup in ML vs. Scala;
2010-11-06, by wenzelm
somewhat more uniform timing in ML vs. Scala;
2010-11-06, by wenzelm
added Markup.Double, Markup.Double_Property;
2010-11-06, by wenzelm
explicit "timing" status for toplevel transactions;
2010-11-06, by wenzelm
tuned;
2010-11-06, by wenzelm
tuned comments;
2010-11-06, by wenzelm
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
2010-11-06, by krauss
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
2010-11-05, by wenzelm
updated keywords;
2010-11-05, by wenzelm
reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi;
2010-11-05, by wenzelm
eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline;
2010-11-05, by wenzelm
reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss;
2010-11-05, by wenzelm
obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views);
2010-11-05, by wenzelm
explicit indication of some remaining violations of the Isabelle/ML interrupt model;
2010-11-05, by wenzelm
updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;
2010-11-05, by wenzelm
proper spelling;
2010-11-05, by wenzelm
merged
2010-11-05, by hoelzl
Extend convex analysis by Bogdan Grechuk
2010-11-05, by hoelzl
merged
2010-11-05, by blanchet
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
2010-11-05, by blanchet
make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
2010-11-05, by blanchet
pass proper type to SMT_Builtin.is_builtin
2010-11-04, by blanchet
remove " s" suffix since seconds are now implicit
2010-11-04, by blanchet
ignore facts with only theory constants in them
2010-11-04, by blanchet
cosmetics
2010-11-04, by blanchet
use the SMT integration's official list of built-ins
2010-11-04, by blanchet
added class relation group_add < cancel_semigroup_add
2010-11-05, by haftmann
merged
2010-11-05, by bulwahn
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
2010-11-05, by bulwahn
added two lemmas about injectivity of concat to the list theory
2010-11-05, by bulwahn
adding documentation of some quickcheck options
2010-11-05, by bulwahn
merged
2010-11-05, by haftmann
Code.check_const etc.: reject too specific types
2010-11-04, by haftmann
corrected quoting
2010-11-04, by haftmann
added lemma length_alloc
2010-11-04, by haftmann
dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
2010-11-04, by haftmann
added note on countable types
2010-11-04, by haftmann
simulate more closely the behaviour of the tactic
2010-11-04, by boehmes
merged
2010-11-04, by wenzelm
merged
2010-11-04, by haftmann
merged
2010-11-04, by haftmann
dropped debug message
2010-11-03, by haftmann
more precise text
2010-11-03, by haftmann
SMLdummy target
2010-11-03, by haftmann
fixed typos
2010-11-03, by haftmann