Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+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.
removed babel again
2008-09-16, by haftmann
celver code lemma avoid type ambiguity problem with Haskell
2008-09-16, by haftmann
a sophisticated char/nibble conversion combinator
2008-09-16, by haftmann
moved term_of syntax to separate theory
2008-09-16, by haftmann
SimpleThread.fork;
2008-09-16, by wenzelm
Simplified thread fork interface.
2008-09-16, by wenzelm
added Concurrent/simple_thread.ML;
2008-09-16, by wenzelm
updated generated file;
2008-09-16, by wenzelm
misc tuning and modernization;
2008-09-16, by wenzelm
check setting and tool;
2008-09-16, by wenzelm
Clearer separation of interpretation frontend and backend.
2008-09-16, by ballarin
No interpretation of locale with dangling type frees.
2008-09-16, by ballarin
Do not rely on locale assumption in interpretation.
2008-09-16, by ballarin
The metis method now fails in the usual manner, rather than raising an exception,
2008-09-16, by paulson
Fixed typo in locale declaration.
2008-09-16, by ballarin
added babel
2008-09-16, by haftmann
explicit size of characters
2008-09-16, by haftmann
dropped superfluous code lemmas
2008-09-16, by haftmann
evaluation using code generator
2008-09-16, by haftmann
generic value command
2008-09-16, by haftmann
converted symbols.tex;
2008-09-15, by wenzelm
tuned;
2008-09-15, by wenzelm
converted misc.tex;
2008-09-15, by wenzelm
tuned;
2008-09-15, by wenzelm
generated files;
2008-09-15, by wenzelm
converted present.tex;
2008-09-15, by wenzelm
basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
2008-09-15, by wenzelm
load underscore package after iman etc.;
2008-09-15, by wenzelm
tuned comment;
2008-09-15, by wenzelm
added formal markup for setting, executable, tool;
2008-09-15, by wenzelm
basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
2008-09-15, by wenzelm
converted basics.tex to theory file;
2008-09-15, by wenzelm
added isatt markup;
2008-09-15, by wenzelm
New outline for codegen tutorial -- draft
2008-09-14, by haftmann
added extern_fact (local or global);
2008-09-12, by wenzelm
print raw (internal) result names;
2008-09-12, by wenzelm
more procise printing of fact names;
2008-09-12, by wenzelm
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
2008-09-12, by wenzelm
cancel, shutdown: notify_all;
2008-09-11, by wenzelm
finish: Future.shutdown last;
2008-09-11, by wenzelm
eliminated requests, use global state variables uniformly;
2008-09-11, by wenzelm
finish: Future.shutdown;
2008-09-11, by wenzelm
added is_empty;
2008-09-11, by wenzelm
shutdown: global join-and-shutdown operation;
2008-09-11, by wenzelm
added focus, which indicates a particular collection of high-priority tasks;
2008-09-11, by wenzelm
some general notes on future values;
2008-09-11, by wenzelm
separate Concurrent/ROOT.ML;
2008-09-11, by wenzelm
Parallel list combinators.
2008-09-11, by wenzelm
added Concurrent/par_list.ML;
2008-09-11, by wenzelm
added interrupt_task (external id);
2008-09-10, by wenzelm
tuned;
2008-09-10, by wenzelm
future_schedule: uninterruptible join;
2008-09-10, by wenzelm
added future_scheduler (default false);
2008-09-10, by wenzelm
replaced join_all by join_results, which returns Exn.results;
2008-09-10, by wenzelm
workers: explicit activity flag;
2008-09-10, by wenzelm
future: allow explicit group;
2008-09-10, by wenzelm
cancel: invalidate group implicitly, via bool ref;
2008-09-10, by wenzelm
auto_flush: uniform block buffering for all output streams;
2008-09-10, by wenzelm
auto_flush stdout, stderr as well;
2008-09-09, by wenzelm
proper values of no_interrupts, regular_interrupts;
2008-09-09, by wenzelm
cancel: check_scheduler;
2008-09-09, by wenzelm
simplified dequeue: provide Thread.self internally;
2008-09-09, by wenzelm
eliminated cache, access queue efficiently via IntGraph.get_first;
2008-09-09, by wenzelm
export get_first from underlying table;
2008-09-09, by wenzelm
out_stream: block-buffered, with separate autoflush thread (every 50ms);
2008-09-09, by wenzelm
babel: removed unnecessary "french" option, which actually enables french section names etc. on some LaTeX installations;
2008-09-09, by wenzelm
added comment
2008-09-09, by nipkow
human-readable printing of TaskQueue.task/group;
2008-09-09, by wenzelm
* Changed defaults for unify configuration options;
2008-09-09, by wenzelm
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
2008-09-09, by wenzelm
job: explicit 'ok' status -- false for canceled jobs;
2008-09-09, by wenzelm
Overall exception handler in order to insulate our users from low-level bugs.
2008-09-09, by paulson
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
2008-09-09, by paulson
Increasing the default limits in order to prevent unnecessary failures.
2008-09-09, by paulson
send: broadcast condition while locked!
2008-09-08, by wenzelm
proper signature constraint;
2008-09-08, by wenzelm
tuned Mailbox.send;
2008-09-08, by wenzelm
removed unused sync_interrupts;
2008-09-08, by wenzelm
moved thread data to future.ML (again);
2008-09-08, by wenzelm
more interrupt operations;
2008-09-08, by wenzelm
moved task, thread_data, group, queue to task_queue.ML;
2008-09-08, by wenzelm
Ordered queue of grouped tasks.
2008-09-08, by wenzelm
added Concurrent/task_queue.ML;
2008-09-08, by wenzelm
await: SYNCHRONIZED wait!
2008-09-08, by wenzelm
tuned check_cache;
2008-09-08, by wenzelm
added sync_interrupts, regular_interrupts;
2008-09-07, by wenzelm
added sync_interrupts, regular_interrupts;
2008-09-07, by wenzelm
opaque signature constraint abstracts local type abbrev;
2008-09-07, by wenzelm
tuned;
2008-09-07, by wenzelm
added change_result;
2008-09-07, by wenzelm
Functional threads as future values.
2008-09-07, by wenzelm
added Concurrent/future.ML;
2008-09-07, by wenzelm
Default (mostly dummy) implementation of thread structures.
2008-09-07, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2008-09-07, by wenzelm
*** empty log message ***
2008-09-07, by wenzelm
explicit use of universal.ML and dummy_thread.ML;
2008-09-07, by wenzelm
added no_interrupts;
2008-09-07, by wenzelm
added no_interrupts;
2008-09-07, by wenzelm
tuned;
2008-09-07, by wenzelm
send: broadcast to all waiting threads;
2008-09-07, by wenzelm
added ML-Systems/thread_dummy.ML;
2008-09-07, by wenzelm
dropped "run" marker in monad syntax
2008-09-06, by haftmann
multithreading.ML provides dummy thread structures;
2008-09-05, by wenzelm
different bookkeeping for code equations
2008-09-05, by haftmann
renamed structure CodeTarget to Code_Target
2008-09-05, by haftmann
instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
2008-09-05, by huffman
proper header;
2008-09-04, by wenzelm
added receive_timeout;
2008-09-04, by wenzelm
check WRAPPER_OUTPUT node type;
2008-09-04, by wenzelm
init: disallow "" as out stream;
2008-09-04, by wenzelm
fixed deps: no Concurrent/receiver.ML yet;
2008-09-04, by wenzelm
Concurrent message exchange via mailbox -- with unbounded queueing.
2008-09-04, by wenzelm
added Concurrent/mailbox.ML;
2008-09-04, by wenzelm
reorganize subsections
2008-09-04, by huffman
rename INF_drop_prefix to INFM_drop_prefix
2008-09-04, by huffman
add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1
2008-09-04, by huffman
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
2008-09-04, by huffman
tuned signature;
2008-09-04, by wenzelm
added General/queue.ML;
2008-09-04, by wenzelm
Efficient queues.
2008-09-04, by wenzelm
moved Multithreading.task/schedule to Concurrent/schedule.ML
2008-09-04, by wenzelm
multithreading.ML provides dummy thread structures;
2008-09-04, by wenzelm
moved Multithreading.task/schedule to Concurrent/schedule.ML;
2008-09-04, by wenzelm
provide dummy thread structures, including proper Thread.getLocal/setLocal;
2008-09-04, by wenzelm
Thread.getLocal/setLocal;
2008-09-04, by wenzelm
Scheduling -- multiple threads working on a queue of tasks.
2008-09-04, by wenzelm
added Concurrent/schedule.ML;
2008-09-04, by wenzelm
update tags
2008-09-03, by convert-repo
use /home/isabelle/mercurial/bin/hg wrapper;
2008-09-03, by wenzelm
exclude large .mov files;
2008-09-03, by wenzelm
simplified add_axiom: no hyps;
2008-09-03, by wenzelm
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
2008-09-03, by wenzelm
axiomatization is now global-only;
2008-09-03, by wenzelm
added const_decl;
2008-09-03, by wenzelm
simplified specify_const: canonical args, global deps;
2008-09-03, by wenzelm
declare_const: Name.binding, store/report position;
2008-09-03, by wenzelm
Sign.declare_const: Name.binding;
2008-09-03, by wenzelm
removed ex/Puzzle
2008-09-03, by nipkow
added qualified: string -> binding -> binding;
2008-09-03, by wenzelm
Name.qualified;
2008-09-03, by wenzelm
theorem dependency hook: check previous state;
2008-09-03, by wenzelm
added pos_of;
2008-09-03, by wenzelm
-> AFP
2008-09-03, by nipkow
simplified Toplevel.add_hook: cover successful transactions only;
2008-09-03, by wenzelm
retired Ben Porter's DenumRat in favour of the shorter proof in
2008-09-03, by kleing
made SML/NJ happy;
2008-09-02, by wenzelm
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
2008-09-02, by wenzelm
* Generic Toplevel.add_hook interface allows to analyze the result of
2008-09-02, by wenzelm
Replaced Library/NatPair by Nat_Int_Bij.
2008-09-02, by nipkow
added new_thms_deps (operates on global facts, some name_hint approximation);
2008-09-02, by wenzelm
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
2008-09-02, by wenzelm
added add_hook interface for post-transition hooks;
2008-09-02, by wenzelm
tuned;
2008-09-02, by wenzelm
ProofDisplay.print_results;
2008-09-02, by wenzelm
no pervasive bindings;
2008-09-02, by wenzelm
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
2008-09-02, by nipkow
distributed literal code generation out of central infrastructure
2008-09-02, by haftmann
* Result facts now refer to the *full* internal name;
2008-09-02, by wenzelm
* Name bindings in higher specification mechanisms;
2008-09-02, by wenzelm
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
2008-09-02, by wenzelm
updated generated file;
2008-09-02, by wenzelm
Interpretation commands no longer accept interpretation attributes.
2008-09-02, by ballarin
type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
added binding;
2008-09-02, by wenzelm
added fixed_decl, fact_decl, local_fact_decl;
2008-09-02, by wenzelm
name_thm etc.: pass position;
2008-09-02, by wenzelm
added type binding -- generic name bindings;
2008-09-02, by wenzelm
name/var morphism operates on Name.binding;
2008-09-02, by wenzelm
adapted to class instantiation compliance
2008-09-02, by haftmann
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
2008-09-01, by nipkow
renamed lemma
2008-09-01, by nipkow
moved more lemmas here from AFP/Integration/Rats
2008-09-01, by nipkow
moved lemma into SetInterval where it belongs
2008-09-01, by nipkow
cleaned up code generation for {.._} and {..<_}
2008-09-01, by nipkow
*** empty log message ***
2008-09-01, by nipkow
extended interface to preferences to allow adding new ones
2008-09-01, by nipkow
Prover is set via menu now
2008-09-01, by nipkow
restructured code generation of literals
2008-09-01, by haftmann
IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
2008-08-29, by wenzelm
init: more explicit protocol of open/remove rendezvous;
2008-08-29, by wenzelm
use hardwired /tmp -- fifo only work on local file-system;
2008-08-29, by wenzelm
separate module for code output
2008-08-29, by haftmann
fixed names of class assumptions
2008-08-29, by haftmann
dropped parameter prefix for class theorems
2008-08-29, by haftmann
added charset (from isabelle_process.scala);
2008-08-28, by wenzelm
moved charset to isabelle_system.scala;
2008-08-28, by wenzelm
provide HOME_JVM=HOME to prevent implicit cygpath mangling;
2008-08-28, by wenzelm
restructured and split code serializer module
2008-08-28, by haftmann
no parameter prefix for class interpretation
2008-08-28, by haftmann
updated
2008-08-28, by haftmann
tuned fold_lines;
2008-08-28, by wenzelm
fold_lines: simplified, more efficient due to String.fields;
2008-08-28, by wenzelm
rm fifo after open;
2008-08-28, by wenzelm
dummy setup for completion;
2008-08-28, by wenzelm
create named pipe;
2008-08-28, by wenzelm
added is_cygwin;
2008-08-28, by wenzelm
join stdout/stderr, eliminated Kind.STDERR;
2008-08-28, by wenzelm
explicit output stream, typically a named pipe;
2008-08-28, by wenzelm
refined option -W: output stream;
2008-08-28, by wenzelm
more function -> fun
2008-08-28, by krauss
quicksort: function -> fun
2008-08-28, by krauss
corrected some typos
2008-08-28, by krauss
fixed atom_to_xml: literal "name" attribute;
2008-08-28, by wenzelm
exported atom_to_xml;
2008-08-28, by wenzelm
changed Markup print mode to YXML -- explicitly decode messages before being issued;
2008-08-28, by wenzelm
tuned;
2008-08-28, by wenzelm
present_token: disable print_mode, which is YXML now;
2008-08-28, by wenzelm
text_of Malformed: explode with spaces -- Output.output/escape ineffective by default;
2008-08-28, by wenzelm
removed obsolete XML.Output workaround;
2008-08-28, by wenzelm
added get_int;
2008-08-28, by wenzelm
removed obsolete get_string;
2008-08-28, by wenzelm
removed obsolete ProofGeneral/pgml_isabelle.ML;
2008-08-28, by wenzelm
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
2008-08-27, by huffman
renamed Buffer.write to File.write_buffer;
2008-08-27, by wenzelm
renamed Buffer.write to File.write_buffer;
2008-08-27, by wenzelm
load buffer.ML before file.ML;
2008-08-27, by wenzelm
replaced find_substring by first_field;
2008-08-27, by wenzelm
Consistent naming of theorems in interpretation.
2008-08-27, by ballarin
simplified parse_attrib (find_substring instead of space_explode);
2008-08-27, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
+30000
tip