Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-384
+384
+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.
merged
2009-09-21, by boehmes
tuned author
2009-09-21, by boehmes
added new method "smt": an oracle-based connection to external SMT solvers
2009-09-18, by boehmes
tuned tracing;
2009-09-20, by wenzelm
scheduler backdoor: 9999 means 1 worker;
2009-09-20, by wenzelm
Hilbert_Classical: more precise control of parallel_proofs;
2009-09-20, by wenzelm
actually observe Multithreading.enabled (cf. d302f1c9e356);
2009-09-20, by wenzelm
merged
2009-09-19, by nipkow
restructured code
2009-09-19, by nipkow
merged
2009-09-19, by haftmann
rewrite premises in tactical proof also with inf_fun_eq and inf_bool_eq: attempt to allow user to use inf [=>] and inf [bool] in his specs
2009-09-18, by haftmann
modified minimization log
2009-09-18, by nipkow
merged
2009-09-18, by nipkow
skip &&& goals
2009-09-18, by nipkow
INTER and UNION are mere abbreviations for INFI and SUPR
2009-09-18, by haftmann
simplified proof
2009-09-18, by haftmann
partially isarified proof
2009-09-18, by haftmann
tuned const_name antiquotations
2009-09-18, by haftmann
more antiquotations
2009-09-18, by haftmann
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
2009-09-18, by haftmann
tuned NEWS, added CONTRIBUTORS
2009-09-18, by haftmann
merged
2009-09-17, by nipkow
removed misleading log line
2009-09-17, by nipkow
NEWS: New method metisFT
2009-09-17, by paulson
New theorems for proving equalities and inclusions involving unions
2009-09-17, by paulson
added time limit for extraction phase (not supported on Cygwin)
2009-09-17, by boehmes
merged
2009-09-17, by boehmes
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
2009-09-17, by boehmes
Synchronized.value does not require locking, since assigments are atomic;
2009-09-16, by wenzelm
tuned;
2009-09-16, by wenzelm
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
2009-09-16, by wenzelm
merged
2009-09-16, by haftmann
Inter and Union are mere abbreviations for Inf and Sup; tuned
2009-09-16, by haftmann
Inter and Union are mere abbreviations for Inf and Sup
2009-09-16, by haftmann
merged
2009-09-16, by nipkow
revised lemma counting
2009-09-16, by nipkow
merged
2009-09-16, by haftmann
merged
2009-09-15, by haftmann
hide new constants
2009-09-15, by haftmann
merged
2009-09-15, by haftmann
restored code generation for OCaml
2009-09-15, by haftmann
added singleton example
2009-09-15, by haftmann
added emptiness check predicate and singleton projection
2009-09-15, by haftmann
added append_after (tuned version of former insert_after of Seq);
2009-09-16, by wenzelm
double linking for improved performance of "prev";
2009-09-15, by wenzelm
merged
2009-09-15, by wenzelm
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
2009-09-15, by boehmes
Isar.define_command: identify transaction;
2009-09-15, by wenzelm
updated bib;
2009-09-15, by wenzelm
count number of iterations required for minimization (and fixed bug: minimization was always called)
2009-09-14, by nipkow
merged
2009-09-14, by haftmann
more antiquotations
2009-09-14, by haftmann
some lemmas about strict order in lattices
2009-09-14, by haftmann
explicitly export type abbreviations (as usual in SML97);
2009-09-13, by wenzelm
wrapper for Real.fmt -- via StringCvt.realfmt;
2009-09-13, by wenzelm
made SML/NJ happy;
2009-09-13, by wenzelm
standard headers and text sections;
2009-09-12, by wenzelm
merged
2009-09-11, by nipkow
Made record parameter flexible to allow for extensions
2009-09-11, by nipkow
merged
2009-09-11, by haftmann
corrected upper/lowercase
2009-09-11, by haftmann
merged
2009-09-10, by haftmann
obey underscore naming convention
2009-09-10, by haftmann
plain structure name; signature constraint; shorter lines
2009-09-10, by haftmann
split of test examples from NatTransfer
2009-09-10, by haftmann
generic transfer procedure
2009-09-10, by haftmann
early bootstrap of generic transfer procedure
2009-09-10, by haftmann
cleanedup theorems all_nat ex_nat
2009-09-10, by haftmann
atp_minimize is now not using whitelist
2009-09-10, by Philipp Meyer
position information is now passed to all actions;
2009-09-10, by nipkow
logging number of metis lemmas
2009-09-10, by nipkow
minimization: comparing w/ and w/o.
2009-09-09, by nipkow
merged
2009-09-09, by haftmann
dropped accidental code additions
2009-09-09, by haftmann
merged
2009-09-09, by haftmann
explicit transfer avoids spurious merge problems
2009-09-09, by haftmann
moved eq handling in nbe into separate oracle
2009-09-09, by haftmann
tuned document -- proper text instead of source comments, reduced line length;
2009-09-08, by wenzelm
fixed cleanup routine in neos csdp script
2009-09-01, by Philipp Meyer
timeout option for ATPs
2009-09-08, by boehmes
merged
2009-09-07, by wenzelm
modernized Event_Bus -- based on actors;
2009-09-07, by wenzelm
Fixed "minimal" to cover the case that "p []" holds (excluded in the article by Bradley & Manna)
2009-09-07, by nipkow
merged
2009-09-07, by nipkow
tuned stats
2009-09-07, by nipkow
Fixed a few problems with the method metisFT
2009-09-07, by paulson
merged
2009-09-07, by nipkow
tuned stats
2009-09-07, by nipkow
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
2009-09-07, by paulson
merged
2009-09-07, by paulson
conflict resolution possibly
2009-09-07, by paulson
New method, metisFT: a fully-typed proof search that should eliminate type errors during reconstruction
2009-09-04, by paulson
merged
2009-08-28, by paulson
More streamlining using metis.
2009-08-27, by paulson
enabled metis permanently, tuned stats
2009-09-07, by nipkow
added signature ATP_MINIMAL,
2009-09-05, by boehmes
merged
2009-09-05, by boehmes
separate output of ATP user time and sledgehammer (ML code) user time
2009-09-05, by boehmes
Mirabelle: command-line action options may either be key=value or just key
2009-09-05, by boehmes
added initialization and cleanup of actions,
2009-09-05, by boehmes
merged
2009-09-04, by haftmann
tuned metis proofs
2009-09-04, by haftmann
tuned
2009-09-04, by boehmes
tuned output
2009-09-04, by nipkow
merged
2009-09-03, by boehmes
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
2009-09-03, by boehmes
merged
2009-09-03, by haftmann
merged
2009-09-03, by haftmann
proper class syntax for sublocale class < expr
2009-09-03, by haftmann
added option full_typed for sledgehammer action
2009-09-03, by boehmes
added runtime information to sledgehammer
2009-09-03, by boehmes
tuned
2009-09-03, by boehmes
scaled avg_time
2009-09-03, by nipkow
merged
2009-09-03, by nipkow
tuned
2009-09-03, by nipkow
isatest: collect test results and logs in testdata repository
2009-09-03, by krauss
replaced backlist by whitelist
2009-09-03, by boehmes
Mirabelle: logging of exceptions (works only for PolyML)
2009-09-03, by boehmes
merged
2009-09-02, by wenzelm
refined delay into delay_first/delay_last;
2009-09-02, by wenzelm
merged
2009-09-02, by boehmes
add report script for Mirabelle
2009-09-02, by boehmes
Mirabelle: actions are responsible for handling exceptions,
2009-09-02, by boehmes
removed errors overseen in previous changes
2009-09-02, by boehmes
moved Mirabelle from HOL/Tools to HOL,
2009-09-02, by boehmes
removed unused signature
2009-09-02, by boehmes
explicit checks;
2009-09-02, by wenzelm
updated Poly/ML SVN version;
2009-09-02, by wenzelm
eval/location_props: always produce YXML markup, independent of print_mode;
2009-09-02, by wenzelm
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
2009-09-02, by wenzelm
tuned ML message;
2009-09-02, by wenzelm
added "using" to blacklist
2009-09-02, by nipkow
merged
2009-09-02, by wenzelm
merged
2009-09-02, by wenzelm
removed old Isar document model;
2009-09-01, by wenzelm
corrected spelling
2009-09-01, by haftmann
merged
2009-09-01, by haftmann
added -q switch for run in qnd mode
2009-09-01, by haftmann
code generator is now a separate component
2009-09-01, by haftmann
tuned document
2009-09-01, by haftmann
some reorganization of number theory
2009-09-01, by haftmann
some reorganization of number theory
2009-09-01, by haftmann
merged
2009-09-01, by haftmann
tuned
2009-09-01, by haftmann
avoid long line
2009-08-24, by haftmann
added txt to blacklist
2009-09-01, by nipkow
Isabelle_Process: receiver as Actor, not EventBus;
2009-09-01, by wenzelm
merged
2009-09-01, by boehmes
Mirabelle: actions are responsible for their log messages, output is better readable
2009-09-01, by boehmes
merged
2009-09-01, by wenzelm
merged
2009-09-01, by boehmes
Mirabelle: added preliminary documentation,
2009-09-01, by boehmes
Mirabelle: explicit command blacklist, preliminary documentation
2009-08-31, by boehmes
modernized Isar_Document;
2009-09-01, by wenzelm
modernized Thy_Header;
2009-09-01, by wenzelm
misc cleanup and internal reorganization;
2009-09-01, by wenzelm
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
2009-09-01, by wenzelm
moved lemma Wellfounded.in_inv_image to Relation.thy
2009-08-31, by krauss
moved wfrec to Recdef.thy
2009-08-31, by krauss
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
2009-08-31, by krauss
Mirabelle: handle possible parser exceptions, emit suitable log message
2009-08-31, by boehmes
merged
2009-08-31, by boehmes
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
2009-08-31, by boehmes
merged
2009-08-31, by nipkow
tuned the simp rules for Int involving insert and intervals.
2009-08-31, by nipkow
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
2009-08-31, by boehmes
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
2009-08-31, by boehmes
merged
2009-08-29, by boehmes
apply metis with found theorems in case sledgehammer was successful
2009-08-29, by boehmes
propagate theorem names, in addition to generated return message
2009-08-29, by boehmes
misc tuning;
2009-08-29, by wenzelm
eliminated hard tabs;
2009-08-29, by wenzelm
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
2009-08-29, by wenzelm
merged
2009-08-28, by wenzelm
fixed HOLogic.stringT
2009-08-28, by krauss
merged
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
tuned proofs
2009-08-28, by nipkow
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
2009-08-28, by nipkow
New option ForceSystem that makes sure we *really* get the system we ask for
2009-08-28, by nipkow
selectable prover for sledgehammer, proper environment lookup
2009-08-28, by boehmes
discontinued Display.pretty_ctyp/cterm etc.;
2009-08-28, by wenzelm
modernized messages -- eliminated ctyp/cterm operations;
2009-08-28, by wenzelm
removed spurious invocations of atp_minimize;
2009-08-28, by wenzelm
removed obsolete print_ctyp, print_cterm;
2009-08-28, by wenzelm
modernized messages -- eliminated old Display.print_cterm;
2009-08-28, by wenzelm
SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
2009-08-28, by wenzelm
misc updates and tuning;
2009-08-28, by wenzelm
PDF_VIEWER: more Unix-ish behaviour on Mac OS;
2009-08-28, by wenzelm
merged
2009-08-27, by nipkow
New example: IMP
2009-08-27, by nipkow
merged
2009-08-27, by nipkow
code generator: quantifiers over {_.._::int} and {_..<_::nat}
2009-08-27, by nipkow
more stats;
2009-08-27, by wenzelm
tuned tracing;
2009-08-27, by wenzelm
merged
2009-08-27, by wenzelm
avoid macbroy21 for now -- hardware problems;
2009-08-27, by wenzelm
tuned code generation for lists
2009-08-27, by nipkow
merged
2009-08-26, by nipkow
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
2009-08-26, by nipkow
merged
2009-08-26, by chaieb
merged
2009-08-26, by chaieb
removed unused theorem finite_Atleast_Atmost
2009-08-26, by chaieb
merged
2009-05-19, by chaieb
Derivative of general reverses
2009-05-19, by chaieb
merged
2009-08-26, by nipkow
new interval lemma
2009-08-26, by nipkow
merged
2009-08-26, by paulson
Simplified some proofs using metis.
2009-08-26, by paulson
merged
2009-08-21, by paulson
sledgehammer used to streamline protocol proofs
2009-08-14, by paulson
Put back characters that had been erased by Emacs
2009-08-14, by paulson
added further conversions and conversionals
2009-08-26, by boehmes
merged
2009-08-26, by nipkow
new lemmas
2009-08-26, by nipkow
some examples for giving measures manually
2009-08-24, by krauss
stricter condition for (binary) integer relation
2009-08-24, by boehmes
more quoting for shell variables, canonical isabelle process
2009-08-24, by boehmes
keep the modified (tested) theory,
2009-08-24, by boehmes
do not introduce additional newlines
2009-08-24, by boehmes
tuned;
2009-08-22, by wenzelm
generalized settings;
2009-08-22, by wenzelm
removed jedit setup -- now a self-contained component (external);
2009-08-22, by wenzelm
less ambitious array operations -- for improved compatibility with older versions of bash;
2009-08-22, by wenzelm
function splitarray: splightly more abstract version that accomodates older bashes;
2009-08-22, by wenzelm
fix IsaMakefile, removing mirabelle (not in HOL/ex/ROOT.ML anyway)
2009-08-21, by krauss
added Mirabelle to NEWS
2009-08-21, by boehmes
merged
2009-08-21, by boehmes
disabled refute action (needs changes in the code of refute)
2009-08-21, by boehmes
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
2009-08-21, by boehmes
moved Mirabelle to HOL/Tools
2009-08-21, by boehmes
moved Mirabelle to HOL/Tools
2009-08-21, by boehmes
Mirabelle tool script conforming to standard Isabelle tool interface,
2009-08-21, by boehmes
made Mirabelle a component
2009-08-17, by boehmes
A few Isar scripts
2009-08-20, by paulson
additional checkpoints avoid problems in error situations
2009-08-15, by haftmann
tuned
2009-08-15, by haftmann
removed atp_minimize invocation
2009-08-14, by krauss
reverted accidential corruption of superscripts introduced in a508148f7c25
2009-08-14, by krauss
merged
2009-08-14, by haftmann
inserted space into message
2009-08-14, by haftmann
formally stylized
2009-08-14, by haftmann
formally stylized
2009-08-14, by haftmann
corrected Pair to Char
2009-08-14, by haftmann
merged
2009-08-14, by webertj
Fixed a bug where the simplifier would hang on
2009-08-14, by webertj
merged
2009-08-13, by paulson
Removal of redundant settings of unification trace and search bounds.
2009-08-13, by paulson
Demonstrations of sledgehammer in protocol proofs.
2009-08-13, by paulson
added PARALLEL_CHOICE, PARALLEL_GOALS;
2009-08-12, by wenzelm
merged
2009-08-11, by wenzelm
SOS: function to set default prover; output channel changed
2009-08-10, by Philipp Meyer
interrupt handler for neos csdp client
2009-08-10, by Philipp Meyer
clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
2009-08-11, by wenzelm
updated generated document
2009-08-11, by haftmann
dropped temporary adjustments to non-working eta expansion in recfun_codegen.ML
2009-08-11, by haftmann
proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
2009-08-11, by haftmann
merged
2009-08-11, by haftmann
temporary adjustment to dubious state of eta expansion in recfun_codegen
2009-08-11, by haftmann
properly merged
2009-08-10, by haftmann
same_typscheme replaces ugly common_typ_eqns
2009-08-10, by haftmann
moved all technical processing of code equations to code_thingol.ML
2009-08-10, by haftmann
added map_transpose
2009-08-10, by haftmann
merged
2009-08-10, by haftmann
attempt to move desymbolization to translation
2009-08-10, by haftmann
added a somehow clueless comment
2009-07-31, by haftmann
repair mess produced by resolution afterwards
2009-07-31, by haftmann
using certify_instantiate
2009-07-31, by haftmann
merged
2009-07-31, by haftmann
cleaned up variable desymbolification and argument expansion
2009-07-31, by haftmann
more appropriate printing of function terms
2009-07-30, by haftmann
improved handling of parameters
2009-07-30, by haftmann
path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
2009-07-30, by haftmann
towards proper handling of argument order in comprehensions
2009-07-30, by haftmann
cleaned up
2009-07-30, by haftmann
termT and term_of_const
2009-07-30, by haftmann
added bij lemmas
2009-08-10, by nipkow
new lemma bij_comp
2009-08-10, by nipkow
refined mac-poly64 tests;
2009-08-08, by wenzelm
tuned spacing of sections;
2009-08-07, by wenzelm
more platforms;
2009-08-06, by wenzelm
tuned header;
2009-08-06, by wenzelm
misc changes to SOS by Philipp Meyer:
2009-08-06, by wenzelm
settings for ATP_Manager component;
2009-08-05, by wenzelm
merged
2009-08-05, by wenzelm
SUBPROOF: recovered Goal.check_finished;
2009-08-05, by wenzelm
added Isabelle_System.components;
2009-08-04, by wenzelm
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
2009-08-04, by wenzelm
etc/components;
2009-08-04, by wenzelm
turned object-logics into components;
2009-08-04, by wenzelm
spelling;
2009-08-04, by wenzelm
tuned "Bootstrapping the environment";
2009-08-04, by wenzelm
change IFS only locally -- thanks to bash arrays;
2009-08-04, by wenzelm
more uniform handling of ISABELLE_HOME_USER component;
2009-08-04, by wenzelm
options for more precise performance figures of at-poly, which happens to run on macbroy21;
2009-08-04, by wenzelm
removing tracing messages in predicate compiler
2009-08-04, by bulwahn
improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging
2009-08-04, by bulwahn
commented rpred compilation; tuned
2009-08-04, by bulwahn
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
2009-08-04, by bulwahn
tuned proof procedure; added size-limiting predicate compilation of higher order predicates; added guessing of number parameters for registrating predicates; removed debug messages
2009-08-04, by bulwahn
changed resolving depending predicates and fetching in the predicate compiler
2009-08-04, by bulwahn
refactoring predicate compiler; repaired proof procedure to handle all test cases
2009-08-04, by bulwahn
refactoring predicate compiler; added type synonyms and functions split_smode and split_mode
2009-08-04, by bulwahn
adapted predicate compiler for quickcheck generators; added compilation of depth-limited search functions for predicates
2009-08-04, by bulwahn
extended mode inference by adding generators; adopted compilation; added some functions for constructing term closures
2009-08-04, by bulwahn
imported patch changed mode inference of predicate compiler to return infered dataflow
2009-08-04, by bulwahn
imported patch generic compilation of predicate compiler with different monads
2009-08-04, by bulwahn
exported functions for quickcheck generator; renamed type constructing functions to fit with the type name in the Predicate theory
2009-08-04, by bulwahn
removed debug messages; exported to_pred in InductiveSet; added further display function; adjusted mode analysis
2009-08-04, by bulwahn
basic support for components (which imitate the usual Isabelle directory layout);
2009-08-04, by wenzelm
Tuned.
2009-08-02, by berghofe
the derived induction principles can be given an explicit name
2009-08-02, by Christian Urban
updated Variable.import;
2009-08-01, by wenzelm
merged
2009-08-01, by wenzelm
merged
2009-08-01, by wenzelm
modernized generated example session;
2009-07-31, by wenzelm
added Mirabelle
2009-07-31, by boehmes
Quickcheck callable from ML
2009-07-31, by boehmes
future scheduler: uninterruptible cancelation;
2009-08-01, by wenzelm
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
2009-08-01, by wenzelm
recovered polyml-5.2 -- need to reload ML-Systems/multithreading.ML after overriding Thread structures;
2009-07-30, by wenzelm
tuned tracing;
2009-07-30, by wenzelm
ISABELLE_USEDIR_OPTIONS: -q 2 by default;
2009-07-30, by wenzelm
merged
2009-07-30, by wenzelm
merged
2009-07-30, by wenzelm
merged
2009-07-30, by haftmann
cleaned up abstract tuple operations and named them consistently
2009-07-29, by haftmann
cleaned up abstract tuple operations and named them consistently
2009-07-29, by haftmann
added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
2009-07-30, by wenzelm
trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;
2009-07-30, by wenzelm
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
2009-07-30, by wenzelm
qualified Subgoal.FOCUS;
2009-07-30, by wenzelm
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
2009-07-30, by wenzelm
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
2009-07-30, by wenzelm
Variable.importT/import: return full instantiations, tuned;
2009-07-30, by wenzelm
added certify_inst, certify_instantiate;
2009-07-30, by wenzelm
merged
2009-07-29, by wenzelm
trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
2009-07-29, by wenzelm
proper Jinja-Slicing;
2009-07-29, by wenzelm
merged
2009-07-29, by wenzelm
merged
2009-07-29, by haftmann
abstractions: desymbolize name hint
2009-07-29, by haftmann
added numeral code postprocessor rules on type int
2009-07-29, by haftmann
sos comments modified
2009-07-29, by nipkow
sos documentation
2009-07-29, by nipkow
Added remote-SOS changes by Philipp Meyer
2009-07-29, by nipkow
Functionality for sum of squares to call a remote csdp prover
2009-07-24, by Philipp Meyer
merged
2009-07-28, by wenzelm
updated generated document
2009-07-28, by haftmann
reinserted legacy ML function
2009-07-28, by haftmann
Set.UNIV and Set.empty are mere abbreviations for top and bot
2009-07-28, by haftmann
explicit is better than implicit
2009-07-28, by haftmann
Meson.first_order_resolve: avoid handle _;
2009-07-29, by wenzelm
removed old global get_claset/map_claset;
2009-07-29, by wenzelm
eliminated METAHYPS;
2009-07-28, by wenzelm
Future.shutdown before loading sequentially -- workaround scheduler deadlock;
2009-07-28, by wenzelm
ResAxioms.neg_conjecture_clauses: proper context;
2009-07-28, by wenzelm
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
2009-07-28, by wenzelm
Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
2009-07-28, by wenzelm
eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
2009-07-28, by wenzelm
non-critical use_thy;
2009-07-28, by wenzelm
future result: Synchronized.var;
2009-07-28, by wenzelm
added unsynchronized Synchronized.peek;
2009-07-28, by wenzelm
group status: Synchronized.var;
2009-07-28, by wenzelm
tuned;
2009-07-28, by wenzelm
Task_Queue.dequeue: explicit thread;
2009-07-28, by wenzelm
more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
2009-07-28, by wenzelm
interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
2009-07-28, by wenzelm
misc tuning;
2009-07-28, by wenzelm
tuned
2009-07-28, by krauss
moved obsolete same_fst to Recdef.thy
2009-07-28, by krauss
adapted doc to type of "op O"
2009-07-28, by krauss
merged
2009-07-28, by wenzelm
merged
2009-07-27, by wenzelm
merged
2009-07-27, by wenzelm
merged
2009-07-27, by wenzelm
added proof of Kleene_Algebra.star_decomp
2009-07-27, by krauss
added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
2009-07-27, by krauss
less
more
|
(0)
-30000
-10000
-3000
-1000
-384
+384
+1000
+3000
+10000
+30000
tip