isabelle: Graph

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
back to polyml-svn -- performance impact is minimal, slowdown was caused by accumulated cruft of long-running Mac OS;
2009-10-30, by wenzelm
less verbose termination tactics
2009-10-30, by krauss
less verbose inductive invocation
2009-10-30, by krauss
tuned
2009-10-30, by krauss
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
2009-10-30, by krauss
merged
2009-10-29, by wenzelm
recovered from 7a1f597f454e, simplified imports;
2009-10-29, by wenzelm
merged
2009-10-29, by wenzelm
merged
2009-10-29, by haftmann
adjusted to changes in theory Divides
2009-10-29, by haftmann
moved some lemmas to theory Int
2009-10-29, by haftmann
moved some dvd [int] facts to Int
2009-10-29, by haftmann
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-29, by haftmann
eliminated some old folds;
2009-10-29, by wenzelm
eliminated some old folds;
2009-10-29, by wenzelm
eliminated some old folds;
2009-10-29, by wenzelm
less aggressive tracing;
2009-10-29, by wenzelm
DEEPEN: less aggressive tracing, subject to trace_DEEPEN;
2009-10-29, by wenzelm
merged
2009-10-29, by wenzelm
merged
2009-10-29, by wenzelm
removing ancient predicate compiler files
2009-10-29, by bulwahn
merged
2009-10-29, by bulwahn
encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
2009-10-29, by bulwahn
improved mode parser; added mode annotations to examples
2009-10-28, by bulwahn
moved datatype mode and string functions to the auxillary structure
2009-10-28, by bulwahn
improving mode parsing in the predicate compiler
2009-10-28, by bulwahn
improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler
2009-10-28, by bulwahn
merged
2009-10-29, by paulson
Tidied up some very ugly proofs
2009-10-29, by paulson
small fixes
2009-10-29, by nipkow
merged
2009-10-29, by haftmann
join entries properly on theory merge
2009-10-29, by haftmann
moved some dvd [int] facts to Int
2009-10-29, by haftmann
moved algebraic classes to Ring_and_Field
2009-10-29, by haftmann
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-29, by haftmann
standardized filter/filter_out;
2009-10-29, by wenzelm
modernized some structure names;
2009-10-29, by wenzelm
eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
2009-10-29, by wenzelm
modernized functor/structures Interpretation;
2009-10-29, by wenzelm
tuned whitespace;
2009-10-29, by wenzelm
unregister: eliminated unused status;
2009-10-29, by wenzelm
proper header;
2009-10-29, by wenzelm
proper header;
2009-10-29, by wenzelm
proper header;
2009-10-29, by wenzelm
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
2009-10-29, by wenzelm
Named_Thms is not scalable;
2009-10-29, by wenzelm
replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space;
2009-10-29, by wenzelm
tuned;
2009-10-29, by wenzelm
tuned proof;
2009-10-29, by wenzelm
separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
2009-10-29, by wenzelm
removed unused file;
2009-10-29, by wenzelm
less hermetic ML;
2009-10-29, by wenzelm
removed slightly exotic symbol abbreviations for now -- achieves a coherent (unique) mapping;
2009-10-29, by wenzelm
simplified method syntax of "smt",
2009-10-29, by boehmes
merged
2009-10-29, by haftmann
adjusted import to changed HOL theory graph
2009-10-29, by haftmann
moved theory Divides after theory Nat_Numeral; tuned some proof texts
2009-10-28, by haftmann
proper nested quotes;
2009-10-28, by wenzelm
components: ensure that the last line is read, even if it lacks EOL;
2009-10-28, by wenzelm
updated Isar.goal;
2009-10-28, by wenzelm
renamed raw Proof.get_goal to Proof.raw_goal;
2009-10-28, by wenzelm
back to Proof.raw_goal;
2009-10-28, by wenzelm
renamed Proof.flat_goal to Proof.simple_goal;
2009-10-28, by wenzelm
Isar.goal: Proof.simple_goal, not raw version;
2009-10-28, by wenzelm
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
2009-10-28, by wenzelm
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
2009-10-28, by wenzelm
slightly more robust error message;
2009-10-28, by wenzelm
tuned;
2009-10-28, by wenzelm
merged
2009-10-28, by wenzelm
merged
2009-10-28, by wenzelm
misc tuning;
2009-10-28, by wenzelm
let naming transform binding beforehand -- covering only the "conceal" flag for now;
2009-10-28, by wenzelm
tuned;
2009-10-28, by wenzelm
simplified default binding;
2009-10-28, by wenzelm
conceal internal bindings;
2009-10-28, by wenzelm
Drule.store: proper binding;
2009-10-28, by wenzelm
added restore_naming;
2009-10-28, by wenzelm
load Product_Type before Nat; dropped junk
2009-10-28, by haftmann
moved lemmas for dvd on nat to theories Nat and Power
2009-10-28, by haftmann
Probability tweaks
2009-10-28, by paulson
merged
2009-10-28, by paulson
New theory Probability, which contains a development of measure theory
2009-10-28, by paulson
merged
2009-10-27, by paulson
New theory SupInf of the supremum and infimum operators for sets of reals.
2009-10-27, by paulson
eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-28, by wenzelm
tuned initial session setup;
2009-10-28, by wenzelm
merged
2009-10-28, by wenzelm
proper headers;
2009-10-28, by wenzelm
reactivated sun-poly, as parallel test;
2009-10-27, by wenzelm
merged
2009-10-27, by wenzelm
merged
2009-10-27, by bulwahn
merged
2009-10-27, by bulwahn
merged
2009-10-27, by bulwahn
merged
2009-10-27, by bulwahn
disabled test case for predicate compiler due to an problem in the inductive package
2009-10-27, by bulwahn
added examples for quickcheck prototype
2009-10-27, by bulwahn
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
2009-10-27, by bulwahn
adding test case for inlining of predicate compiler
2009-10-27, by bulwahn
hiding randompred definitions
2009-10-27, by bulwahn
changes to example file
2009-10-27, by bulwahn
print retrieved specification when printing intermediate results
2009-10-27, by bulwahn
added option show_modes to predicate compiler
2009-10-27, by bulwahn
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
2009-10-27, by bulwahn
removed unused file smt_builtin.ML,
2009-10-27, by boehmes
included description for sledgehammer options in Mirabelle script
2009-10-27, by boehmes
measure runtime of ATPs only if requested
2009-10-27, by boehmes
eliminated some old folds;
2009-10-27, by wenzelm
eliminated some old folds;
2009-10-27, by wenzelm
Datatype.read_typ: standard argument order;
2009-10-27, by wenzelm
normalized basic type abbreviations;
2009-10-27, by wenzelm
misc tuning and simplification;
2009-10-27, by wenzelm
merged
2009-10-27, by wenzelm
merged
2009-10-27, by wenzelm
merged
2009-10-27, by haftmann
merged
2009-10-27, by haftmann
tuned
2009-10-27, by haftmann
tuned
2009-10-27, by haftmann
dropped obsolete comment
2009-10-27, by haftmann
added implode and explode
2009-10-27, by haftmann
added friendly error message when Kodkodi is not available
2009-10-27, by blanchet
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
2009-10-27, by blanchet
merged
2009-10-27, by blanchet
merged
2009-10-26, by blanchet
made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
2009-10-26, by blanchet
more thread-safe access to global refs;
2009-10-27, by wenzelm
avoid structure alias;
2009-10-27, by wenzelm
comment;
2009-10-27, by wenzelm
non-critical output -- ship message in one piece;
2009-10-27, by wenzelm
ProofContext.setmp_verbose_CRITICAL;
2009-10-27, by wenzelm
non-critical atomic accesses;
2009-10-27, by wenzelm
critical comments;
2009-10-27, by wenzelm
tuned;
2009-10-27, by wenzelm
SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace;
2009-10-27, by wenzelm
max_threads_value: eliminated tested_platform -- Poly/ML 5.3 fully supports linux, darwin, solaris, cygwin;
2009-10-27, by wenzelm
lemma converse_inv_image
2009-10-26, by krauss
authentic constants; moved "acyclic" further down
2009-10-26, by krauss
point-free characterization of well-foundedness
2009-10-26, by krauss
replaced (outdated) comments by explicit statements
2009-10-26, by krauss
reactivated test on sunbroy2 -- with full proof parallelism (requires Poly/ML-SVN-921);
2009-10-26, by wenzelm
forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;
2009-10-26, by wenzelm
tuned;
2009-10-26, by wenzelm
added nitpick manual here;
2009-10-26, by wenzelm
recovered sort indentation for "sort position", as documented in the file;
2009-10-26, by wenzelm
tuned white space;
2009-10-26, by wenzelm
merged
2009-10-26, by haftmann
merged
2009-10-26, by haftmann
avoid upto if not needed
2009-10-26, by haftmann
conceal quickcheck generators
2009-10-26, by haftmann
merged
2009-10-26, by blanchet
merged
2009-10-26, by blanchet
make Nitpick compile again
2009-10-26, by blanchet
merged
2009-10-26, by blanchet
be somewhat more liberal in Nitpick about which types may occur in formulas
2009-10-23, by blanchet
make the Nitpick examples work again
2009-10-23, by blanchet
updated keyword files to include "nitpick" and "nitpick_params"
2009-10-23, by blanchet
continuation of Nitpick's integration into Isabelle;
2009-10-23, by blanchet
updated Nitpick documentation to remove weird default for "overlord"
2009-10-23, by blanchet
updated Nitpick manual to reflect the latest Stand der Dinge
2009-10-23, by blanchet
merged
2009-10-22, by blanchet
wrap line correctly in Nitpick documentation
2009-10-22, by blanchet
added Nitpick's theory and ML files to Isabelle/HOL;
2009-10-22, by blanchet
Added Nitpick manual.
2009-10-22, by blanchet
merged
2009-10-26, by berghofe
Added Pattern.thy to Nominal/Examples.
2009-10-26, by berghofe
merged
2009-10-26, by haftmann
tuned
2009-10-26, by haftmann
added SML_Quickcheck import
2009-10-26, by haftmann
tuned code setup for primitive boolean connectors
2009-10-26, by haftmann
legacy warnings for old-style term styles
2009-10-26, by haftmann
removed unnecessary NameSpace prefix;
2009-10-26, by wenzelm
misc tuning and updates;
2009-10-26, by wenzelm
merged
2009-10-26, by wenzelm
implicit default is 4 cores -- more cost-effective;
2009-10-26, by wenzelm