isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

added documentation for local SMT solver setup and available SMT options,
2009-11-06, by boehmes
renamed method induct_scheme to induction_schema
2009-11-06, by krauss
NEWS
2009-11-06, by krauss
removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)
2009-11-06, by krauss
renamed method sizechange to size_change
2009-11-06, by krauss
added boehmes and hoelzl to isatest mailings
2009-11-06, by krauss
merged
2009-11-06, by wenzelm
tuned
2009-11-06, by boehmes
Merged.
2009-11-05, by ballarin
Merged.
2009-11-04, by ballarin
Use PrintMode.setmp to make thread-safe; avoid code clones.
2009-11-04, by ballarin
Make output indenpendent of current print mode.
2009-11-02, by ballarin
Relax on type agreement with original context when applying term syntax.
2009-11-02, by ballarin
tuned;
2009-11-05, by wenzelm
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
2009-11-05, by wenzelm
adapted LocalTheory.declaration;
2009-11-05, by wenzelm
allow "pervasive" local theory declarations, which are applied the background theory;
2009-11-05, by wenzelm
declare Spec_Rules for most basic definitional packages;
2009-11-05, by wenzelm
misc tuning and clarification;
2009-11-05, by wenzelm
scalable version of Named_Thms, using Item_Net;
2009-11-05, by wenzelm
merged
2009-11-05, by wenzelm
merged
2009-11-05, by wenzelm
more accurate cleanup;
2009-11-05, by wenzelm
merged
2009-11-05, by wenzelm
more accurate dependencies;
2009-11-05, by wenzelm
merged
2009-11-05, by boehmes
handle let expressions inside terms by unfolding (instead of raising an exception),
2009-11-05, by boehmes
shorter names for variables and verification conditions,
2009-11-05, by boehmes
added references to HOL-Boogie papers
2009-11-05, by boehmes
tuned header;
2009-11-05, by wenzelm
made SML/NJ happy;
2009-11-05, by wenzelm
eliminated funny record patterns and made SML/NJ happy;
2009-11-05, by wenzelm
proper header;
2009-11-05, by wenzelm
more accurate dependencies;
2009-11-05, by wenzelm
merged
2009-11-05, by wenzelm
added Tree23 to IsaMakefile
2009-11-04, by krauss
New
2009-11-04, by nipkow
merged
2009-11-04, by nipkow
fixed order of parameters in induction rules
2009-11-04, by nipkow
added bulwahn to isatest mailings
2009-11-04, by krauss
merged
2009-11-04, by nipkow
Completely overhauled
2009-11-04, by nipkow
better error handling for fixrec_simp
2009-11-03, by huffman
add more fixrec_simp rules
2009-11-03, by huffman
fixrec examples use fixrec_simp instead of fixpat
2009-11-03, by huffman
domain package registers fixrec_simp lemmas
2009-11-03, by huffman
merged
2009-11-03, by huffman
add fixrec_simp attribute and method (eventually to replace fixpat)
2009-11-03, by huffman
proper and unique case names for the split_vc method,
2009-11-03, by boehmes
merged
2009-11-03, by haftmann
merged
2009-11-03, by haftmann
always be qualified -- suspected smartness in fact never worked as expected
2009-11-03, by haftmann
pretty name for ==>
2009-11-03, by haftmann
added HOL-Boogie
2009-11-03, by boehmes
added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception),
2009-11-03, by boehmes
ignore parsing errors, return empty assignment instead
2009-11-03, by boehmes
scheduler: clarified interrupt attributes and handling;
2009-11-05, by wenzelm
worker_next: plain signalling via work_available only, not scheduler_event;
2009-11-05, by wenzelm
revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);
2009-11-05, by wenzelm
avoid broadcast work_available, use daisy-chained signal instead;
2009-11-04, by wenzelm
fulfill_proof_future: tuned important special case of singleton promise;
2009-11-04, by wenzelm
worker_next: treat wait for work_available as Sleeping, not Waiting;
2009-11-04, by wenzelm
worker activity: distinguish between waiting (formerly active) and sleeping;
2009-11-04, by wenzelm
tuned;
2009-11-04, by wenzelm
tuned thread data;
2009-11-04, by wenzelm
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
2009-11-04, by wenzelm
slightly leaner and more direct control of worker activity etc.;
2009-11-03, by wenzelm
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
2009-11-03, by bulwahn
adapted the inlining in the predicate compiler
2009-11-03, by bulwahn
recursively replacing abstractions by new definitions in the predicate compiler
2009-11-03, by bulwahn
merge
2009-11-02, by huffman
add fixrec support for HOL pair constructor patterns
2009-11-02, by huffman
define cprod_fun using Pair instead of cpair
2009-11-02, by huffman
add (LAM (x, y). t) syntax and lemma csplit_Pair
2009-11-02, by huffman
lexicographic order: run local descent proofs in parallel
2009-11-02, by krauss
merged
2009-11-02, by huffman
domain package no longer uses cfst/csnd/cpair
2009-11-02, by huffman
conceal partial rules depending on config flag (i.e. when called via "fun")
2009-11-02, by krauss
conceal "termination" rule, used only by special tools
2009-11-02, by krauss
do not use Binding.empty: conceal flag gets lost in Thm.def_binding_optional
2009-11-02, by krauss
modernized structure XML_Syntax;
2009-11-02, by wenzelm
structure Thm_Deps;
2009-11-02, by wenzelm
modernized structure Proof_Node;
2009-11-02, by wenzelm
modernized structure Proof_Display;
2009-11-02, by wenzelm
modernized structure Proof_Syntax;
2009-11-02, by wenzelm
modernized structure Local_Syntax;
2009-11-02, by wenzelm
modernized structure AutoBind;
2009-11-02, by wenzelm
modernized structure Primitive_Defs;
2009-11-02, by wenzelm
modernized structure Simple_Syntax;
2009-11-02, by wenzelm
modernized structure Context_Position;
2009-11-02, by wenzelm
observe usual naming conventions;
2009-11-02, by wenzelm
find_theorems: respect conceal flag
2009-11-02, by krauss
DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);
2009-11-02, by wenzelm
back to warning -- Proof General tends to "popup" tracing output;
2009-11-02, by wenzelm
split parsing of counterexamples from translation into terms (avoids Term.dummyT and ill-typed terms)
2009-11-02, by boehmes
merged
2009-11-02, by bulwahn
predicate compiler creates code equations for predicates with full mode
2009-10-31, by bulwahn
renamed rpred to random
2009-10-30, by bulwahn
Rules that characterize functional/relational specifications.
2009-11-01, by wenzelm
adapted Item_Net;
2009-11-01, by wenzelm
allow multi-index;
2009-11-01, by wenzelm
added insert_safe, delete_safe variants;
2009-11-01, by wenzelm
tuned signature;
2009-11-01, by wenzelm
modernized structure Context_Rules;
2009-11-01, by wenzelm
modernized structure Rule_Cases;
2009-11-01, by wenzelm
merged
2009-10-30, by haftmann
dedicated theory for loading numeral simprocs
2009-10-30, by haftmann
set Pure theory name properly
2009-10-30, by haftmann
tuned code setup
2009-10-30, by haftmann
some notes on SPASS 3.0 distribution;
2009-10-30, by wenzelm
merged
2009-10-30, by haftmann
combined former theories Divides and IntDiv to one theory Divides
2009-10-30, by haftmann
tuned variable names of bindings; conceal predicate constants
2009-10-30, by haftmann
dedicated theory for loading numeral simprocs
2009-10-30, by haftmann
moved some div/mod lemmas to theory Divides
2009-10-30, by haftmann
tuned proof
2009-10-30, by haftmann
moved Commutative_Ring into session Decision_Procs
2009-10-30, by haftmann
abstract over variables in reversed order (application uses given order)
2009-10-30, by boehmes
disable printing of unparsed counterexamples for CVC3 and Yices
2009-10-30, by boehmes
pattern are separated only by spaces (no comma)
2009-10-30, by boehmes