Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-192
+192
+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.
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
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-192
+192
+1000
+3000
+10000
+30000
tip