isabelle: Graph

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
added find_substring;
2008-08-27, by wenzelm
added HOL/ex/Numeral.thy
2008-08-27, by haftmann
get rid of tabs;
2008-08-27, by wenzelm
Property lists.
2008-08-27, by wenzelm
added General/properties.ML;
2008-08-27, by wenzelm
type Properties.T;
2008-08-27, by wenzelm
proper error message
2008-08-27, by haftmann
proper handling of type variabl names
2008-08-27, by haftmann
completing arities after subclass instance
2008-08-27, by haftmann
untabification
2008-08-27, by haftmann
tuned code generator setup
2008-08-27, by haftmann
added equivariance lemmas for ex1 and the
2008-08-27, by urbanc
add lemmas about Rats similar to those about Reals
2008-08-27, by huffman
move real_vector class proofs into vector_space and group_hom locales
2008-08-26, by huffman
added distributivity of relation composition over union [simp]
2008-08-26, by krauss
tuned append;
2008-08-26, by wenzelm
command: symbols.encode;
2008-08-26, by wenzelm
Reorganisation of registration code.
2008-08-26, by ballarin
function package: name primitive defs "f_sumC_def" instead of "f_sum_def" to avoid clashes
2008-08-26, by krauss
purge classes after compilation;
2008-08-26, by wenzelm
renamed Isabelle-repository to isabelle;
2008-08-26, by wenzelm
Defined rationals (Rats) globally in Rational.
2008-08-26, by nipkow
replaced /home/isabelle/html-data/isabelle-repos by /home/isabelle-repository/repos;
2008-08-26, by wenzelm
moved new Symbol.Interpretation into plugin;
2008-08-25, by wenzelm
promoted to EBPlugin;
2008-08-25, by wenzelm
explicitly depend on isabelle-Pure.jar and isabelle-scala-library.jar;
2008-08-25, by wenzelm
tuned;
2008-08-25, by wenzelm
isabelle process: pick options/args from properties;
2008-08-25, by wenzelm
removed unused ConsolePlugin dependency;
2008-08-25, by wenzelm
simplified exceptions: use plain error function / RuntimeException;
2008-08-25, by wenzelm
added try_result;
2008-08-25, by wenzelm
misc reorganization;
2008-08-24, by wenzelm
Kind: added is_control;
2008-08-24, by wenzelm
get: allow null;
2008-08-24, by wenzelm
misc tuning of names;
2008-08-24, by wenzelm
rearranged source files;
2008-08-24, by wenzelm
init_message: class markup in message body, not header;
2008-08-24, by wenzelm
repackaged as isabelle.jedit;
2008-08-24, by wenzelm
untabify: silently turn tab into space if column information is unavailable;
2008-08-24, by wenzelm
corrected cache handling for class operations
2008-08-24, by haftmann
default replaces arbitrary
2008-08-24, by haftmann
tuned import order
2008-08-24, by haftmann
activated \<A>, \<a>, \<AA>, \<aa>;
2008-08-24, by wenzelm
* Isabelle/lib/classes/Pure.jar;
2008-08-23, by wenzelm
jars: removed obsolete Java process wrapper (cf. new Pure.jar);
2008-08-23, by wenzelm
obsolete;
2008-08-23, by wenzelm
obsolete -- superceded by Pure.jar (Scala version);
2008-08-23, by wenzelm
updated to Pure.jar;
2008-08-23, by wenzelm
added exec;
2008-08-23, by wenzelm
moved class Result into static object, removed dynamic tree method;
2008-08-23, by wenzelm
symbolic message markup;
2008-08-23, by wenzelm
renamed Markup.MALFORMED to Markup.BAD;
2008-08-23, by wenzelm
added position, messages;
2008-08-23, by wenzelm
added messages and process information;
2008-08-23, by wenzelm
Position properties.
2008-08-23, by wenzelm
added General/position.scala;
2008-08-23, by wenzelm
adapted to new IsabelleProcess from Pure.jar;
2008-08-23, by wenzelm
include ../../classes/Pure.jar;
2008-08-23, by wenzelm
added const Rational
2008-08-23, by nipkow
YXML.parse_failsafe;
2008-08-23, by wenzelm
shell_prefix: physical /bin/env on Cygwin;
2008-08-23, by wenzelm
removed full_markup mode (default);
2008-08-23, by wenzelm
added parse_failsafe;
2008-08-23, by wenzelm
refer to symbolic Markup;
2008-08-23, by wenzelm
Common markup elements.
2008-08-23, by wenzelm
added General/markup.scala;
2008-08-23, by wenzelm
BadVariable: toString;
2008-08-23, by wenzelm
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
2008-08-23, by wenzelm
append_string: proper backslash in character escapes;
2008-08-23, by wenzelm
added getenv;
2008-08-23, by wenzelm
tuned;
2008-08-23, by wenzelm
Isabelle outer syntax.
2008-08-23, by wenzelm
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
2008-08-23, by wenzelm
Isabelle process management -- always reactive due to multi-threaded I/O.
2008-08-23, by wenzelm
renamed DOM to document, add xml version and optional stylesheets;
2008-08-23, by wenzelm
tuned comments;
2008-08-22, by wenzelm
parse_attrib: proper index of name end!
2008-08-21, by wenzelm
tuned parse performance: avoid splitting terminal Y chunk;
2008-08-21, by wenzelm
parse_attrib: more efficient due to indexOf('=');
2008-08-21, by wenzelm
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
2008-08-21, by wenzelm
tuned comment;
2008-08-21, by wenzelm
added iterator over content;
2008-08-21, by wenzelm
proper ISABELLE_ROOT_JVM on Cygwin;
2008-08-21, by wenzelm
pattern: proper "." not "[.]"!
2008-08-21, by wenzelm
recode: proper result for unmatched symbols;
2008-08-21, by wenzelm
more robust pattern: look at longer matches first, added catch-all case;
2008-08-21, by wenzelm
added get_setting;
2008-08-21, by wenzelm
read_symbols: proper IsabelleSystem.platform_path;
2008-08-21, by wenzelm