isabelle: Graph

removed some old settings;
2010-11-27, by wenzelm
recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
2010-11-27, by wenzelm
merged
2010-11-26, by huffman
remove map function names from domain package theory data
2010-11-26, by huffman
isar-style proof for lemma contI2
2010-11-26, by huffman
remove case combinator for fixrec match type
2010-11-26, by huffman
declare more simp rules for powerdomains
2010-11-26, by huffman
merged;
2010-11-27, by wenzelm
merged
2010-11-26, by haftmann
strict forall2
2010-11-26, by haftmann
nbe decides equality of abstractions by extensionality
2010-11-26, by haftmann
eliminated some generated comments;
2010-11-26, by wenzelm
merged
2010-11-26, by wenzelm
merged
2010-11-26, by haftmann
keep type variable arguments of datatype constructors in bookkeeping
2010-11-26, by haftmann
document changes in Nitpick and MESON/Metis
2010-11-26, by blanchet
renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first
2010-11-26, by blanchet
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
2010-11-26, by blanchet
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-26, by wenzelm
just one version of fold_rev2;
2010-11-26, by wenzelm
explicit use of unprefix;
2010-11-26, by wenzelm
keep private things private, without comments;
2010-11-26, by wenzelm
eliminated some clones of eq_list;
2010-11-26, by wenzelm
merged
2010-11-26, by nipkow
new lemma
2010-11-26, by nipkow
lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
2010-11-26, by wenzelm
prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
2010-11-26, by wenzelm
discontinued global "Isabelle" symlink, to make each distribution even more self-contained;
2010-11-26, by wenzelm
more correct spelling;
2010-11-26, by wenzelm
globbing constant expressions use more idiomatic underscore rather than star
2010-11-26, by haftmann
globbing constant expressions use more idiomatic underscore rather than star;
2010-11-26, by haftmann
datatype constructor glob for code_reflect
2010-11-26, by haftmann
merged
2010-11-26, by haftmann
merged
2010-11-26, by haftmann
merged
2010-11-25, by haftmann
toplevel deresolving for flat module name space
2010-11-25, by haftmann
merged
2010-11-26, by hoelzl
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
2010-11-23, by hoelzl
Replace surj by abbreviation; remove surj_on.
2010-11-22, by hoelzl
adjust Sledgehammer/SMT fudge factor
2010-11-26, by blanchet
clarified Par_List.managed_results, with explicit propagation of outermost physical interrupt to forked futures (e.g. to make timeout apply here as expected and prevent zombies);
2010-11-25, by wenzelm
merge
2010-11-25, by blanchet
cosmetics
2010-11-25, by blanchet
eta-reduce on the fly to prevent an exception
2010-11-25, by blanchet
merged
2010-11-25, by nipkow
Added the simplest finite Ramsey theorem
2010-11-25, by nipkow
reverted c059d550afec -- the triviality check had apparently nothing to do with spontaneous Interrupt exceptions
2010-11-25, by blanchet
set Metis option on correct context, lest it be ignored
2010-11-25, by blanchet
make "debug" mode of Sledgehammer/SMT more liberal
2010-11-25, by blanchet
fix check for builtinness of 0 and 1 -- these aren't functions
2010-11-25, by blanchet
added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway
2010-11-25, by blanchet
document requirement on theory import
2010-11-24, by blanchet
corrected abd4e7358847 where SOMEthing went utterly wrong
2010-11-24, by haftmann
merged
2010-11-24, by boehmes
swap names for built-in tester functions (to better reflect the intuition of what they do);
2010-11-24, by boehmes
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
2010-11-24, by boehmes
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
2010-11-24, by blanchet
removing Enum.in_enum from the claset
2010-11-24, by bulwahn
merged
2010-11-24, by boehmes
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-24, by boehmes
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
2010-11-24, by boehmes
announcing some latest change (d40b347d5b0b)
2010-11-24, by bulwahn
merged
2010-11-23, by blanchet
more precise characterization of built-in constants "number_of", "0", and "1"
2010-11-23, by blanchet
merged
2010-11-23, by haftmann
merged
2010-11-22, by haftmann
adhere established Collect/mem convention more closely
2010-11-22, by haftmann
merged
2010-11-22, by haftmann
replaced misleading Fset/fset name -- these do not stand for finite sets
2010-11-22, by haftmann
renamed slightly ambivalent crel to effect
2010-11-22, by haftmann
disable triviality checking -- it might be the source of the spurious Interrupt exceptions that make it almost impossible to run Judgement Day
2010-11-23, by blanchet
more precise error handling for Z3;
2010-11-23, by blanchet
use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on
2010-11-23, by blanchet
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
2010-11-23, by blanchet
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
2010-11-23, by blanchet
added "verbose" option to Metis to shut up its warnings if necessary
2010-11-23, by blanchet
added support for quantifier weight annotations
2010-11-22, by boehmes
share and use more utility functions;
2010-11-22, by boehmes
added prove reconstruction for injective functions;
2010-11-22, by boehmes
generous timeout gives more breath in parallel run on less luxury machines
2010-11-22, by haftmann
adding setup for exhaustive testing in example file
2010-11-22, by bulwahn
hiding enum
2010-11-22, by bulwahn
adapting example in Predicate_Compile_Examples
2010-11-22, by bulwahn
hiding the constants
2010-11-22, by bulwahn
improving function is_iterable in quickcheck
2010-11-22, by bulwahn
adding temporary options to the quickcheck examples
2010-11-22, by bulwahn
adapting the quickcheck examples
2010-11-22, by bulwahn
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
2010-11-22, by bulwahn
adding code equations for EX1 on finite types
2010-11-22, by bulwahn
adding code equation for function equality; adding some instantiations for the finite types
2010-11-22, by bulwahn
adding Enum to HOL-Main image and removing it from HOL-Library
2010-11-22, by bulwahn
moving Enum theory from HOL/Library to HOL
2010-11-22, by bulwahn
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
2010-11-22, by bulwahn
adding prototype for finite_type instantiations
2010-11-22, by bulwahn
adding option finite_types to quickcheck
2010-11-22, by bulwahn
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
2010-11-22, by bulwahn
changed old-style quickcheck configurations to new Config.T configurations
2010-11-22, by bulwahn
adding temporary function test_test_small to Quickcheck
2010-11-22, by bulwahn
added useful function map_context_result to signature
2010-11-22, by bulwahn
moving the error handling to the right scope in smallvalue_generators
2010-11-22, by bulwahn
removing clone from function package and using the clean interface from Function_Relation instead
2010-11-22, by bulwahn
adding function generation to SmallCheck; activating exhaustive search space testing
2010-11-22, by bulwahn
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
2010-11-22, by bulwahn
generalized ensure_random_datatype to ensure_sort_datatype
2010-11-22, by bulwahn
renaming quickcheck generator code to random
2010-11-22, by bulwahn
ported sledgehammer_tactic to current development version
2010-11-22, by bulwahn
adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
2010-11-22, by bulwahn
adding files to use sledgehammer as a tactic for non-interactive use
2010-11-22, by bulwahn
adding birthday paradoxon from some abandoned drawer
2010-11-22, by bulwahn
adding extensional function spaces to the FuncSet library theory
2010-11-22, by bulwahn
tuned
2010-11-22, by haftmann
tuned
2010-11-22, by haftmann
updated explode vs. raw_explode;
2010-11-20, by wenzelm
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-20, by wenzelm
total Symbol.explode (cf. 1050315f6ee2);
2010-11-19, by wenzelm
do not export Thy_Load.required, to avoid confusion about the interface;
2010-11-19, by wenzelm
merged
2010-11-19, by huffman
declare adm_chfin [simp]
2010-11-17, by huffman
add lemma cont_fun; remove unused lemma monofun_app
2010-11-17, by huffman
accumulated NEWS updates for HOLCF
2010-11-17, by huffman
section -> subsection
2010-11-17, by huffman
add lemma adm_prod_case
2010-11-17, by huffman
merged
2010-11-19, by paulson
First-order pattern matching: catch a rogue exception (differing numbers of arguments)
2010-11-19, by paulson
eval simp rules for predicate type, simplify primitive proofs
2010-11-19, by haftmann
generalized type
2010-11-19, by haftmann
made smlnj happy
2010-11-19, by haftmann
merged
2010-11-19, by haftmann
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
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