isabelle: Graph

do not buffer fifo streams here -- done in Isabelle_Process;
2010-08-13, by wenzelm
explicit Document.State value, instead of individual state variables in Session, Command, Document;
2010-08-13, by wenzelm
edit_document: more precise status position;
2010-08-13, by wenzelm
added get_after convenience;
2010-08-13, by wenzelm
more basic notion of unparsed input;
2010-08-12, by wenzelm
simplified/clarified Change: transition prev --edits--> result, based on futures;
2010-08-12, by wenzelm
moved snapshot to Session (cf. 96b22dfeb56a);
2010-08-12, by wenzelm
Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway;
2010-08-12, by wenzelm
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
2010-08-12, by wenzelm
misc tuning and simplification;
2010-08-12, by wenzelm
specific command state;
2010-08-12, by wenzelm
specific Session.Commands_Changed;
2010-08-12, by wenzelm
consider snapshot as service of Session, not Document.Change;
2010-08-12, by wenzelm
tuned scope;
2010-08-12, by wenzelm
Document.print_id;
2010-08-11, by wenzelm
consider command state as part of Snapshot, not Document;
2010-08-11, by wenzelm
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
2010-08-11, by wenzelm
Named_Target;
2010-08-11, by wenzelm
modernized specifications;
2010-08-11, by wenzelm
spelling;
2010-08-11, by wenzelm
merged
2010-08-11, by wenzelm
renamed Theory_Target to the more appropriate Named_Target
2010-08-11, by haftmann
discontinue old implementation of `foundation`
2010-08-11, by haftmann
moved instantiation target formally to class_target.ML
2010-08-11, by haftmann
NEWS
2010-08-11, by haftmann
merged
2010-08-11, by haftmann
print fcomp combinator only monadic in connection with other monadic expressions
2010-08-11, by haftmann
merged
2010-08-11, by haftmann
merged
2010-08-11, by haftmann
moved overloading target formally to overloading.ML
2010-08-11, by haftmann
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
2010-08-11, by haftmann
merged
2010-08-11, by haftmann
whitespace tuning
2010-08-11, by haftmann
remove overloading and instantiation from data slot
2010-08-11, by haftmann
removed obsolete Toplevel.enter_proof_body;
2010-08-11, by wenzelm
standardized pretty printing of consts (e.g. see find_theorems, print_theory);
2010-08-11, by wenzelm
misc tuning and simplification;
2010-08-11, by wenzelm
simplified/unified command setup;
2010-08-11, by wenzelm
removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);
2010-08-11, by wenzelm
prefer plain Attrib.eval_thmss -- also means the assert_forward of Proof.get_thmss_cmd is skipped, leading to uniform (albeit odd) behaviour concerning forward chaining;
2010-08-11, by wenzelm
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
2010-08-11, by wenzelm
tuned eval_thms (cf. note etc. in proof.ML);
2010-08-11, by wenzelm
use Pretty.enum convenience;
2010-08-11, by wenzelm
tuned whitespace;
2010-08-11, by wenzelm
more precise and more maintainable dependencies;
2010-08-11, by wenzelm
merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;
2010-08-11, by wenzelm
* -> prod
2010-08-11, by haftmann
added .ML extension
2010-08-11, by haftmann
avoid old unnamed infix
2010-08-11, by haftmann
avoid inclusion of Natural module in generated code
2010-08-11, by haftmann
explicit ML extension
2010-08-11, by haftmann
merged
2010-08-11, by haftmann
separate initialisation for overloading and instantiation target
2010-08-10, by haftmann
different foundations for different targets; simplified syntax handling of abbreviations
2010-08-10, by haftmann
deleted duplicate lemma
2010-08-11, by Christian Urban
Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
2010-08-10, by ballarin
basic renumbering
2010-08-10, by haftmann
avoiding redundant primes
2010-08-10, by haftmann
separated type from term parameters
2010-08-10, by haftmann
moved extra_tfrees check for mixfix syntax to Generic_Target
2010-08-10, by haftmann
name and argument grouping tuning
2010-08-10, by haftmann
whitespace tuning
2010-08-10, by haftmann
added generic_target.ML
2010-08-10, by haftmann
try to uniformly follow define/note/abbrev/declaration order as close as possible
2010-08-10, by haftmann
split off structure Generic_Target into separate file
2010-08-10, by haftmann
split off generic parts of target implementations into separate structure
2010-08-10, by haftmann
restructured code for `declaration`
2010-08-10, by haftmann
executable relation operations contributed by Tjark Weber
2010-08-10, by haftmann
factored out foundation of `define` into separate function
2010-08-09, by haftmann
combine declaration and definition of foundation constant
2010-08-09, by haftmann
more appropriate outline of `define`
2010-08-09, by haftmann
backlink definition to target `notes`
2010-08-09, by haftmann
merged
2010-08-09, by haftmann
dropped idle local_facts argument; factored out theory_abbrev and locale_abbrev
2010-08-09, by haftmann
more convenient order
2010-08-09, by haftmann
dropped misleading comments
2010-08-09, by haftmann
merged
2010-08-09, by haftmann
separated foundation of `notes`
2010-08-09, by haftmann
more clear separation into local and global facts
2010-08-09, by haftmann
sharpened and tuned educated guess for canonical class morphism
2010-08-09, by haftmann
minimize sorts in certificate instantiation
2010-08-09, by haftmann
prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
2010-08-09, by blanchet
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
2010-08-09, by blanchet
"declare" -> "declaration" (typo)
2010-08-09, by blanchet
replace "setup" with "declaration"
2010-08-09, by blanchet
disable Nitpick on Cygwin while I'm on vacation;
2010-08-09, by blanchet
merged
2010-08-09, by blanchet
use "declaration" instead of "setup" to register Nitpick extensions
2010-08-09, by blanchet
remove needless "open"
2010-08-09, by blanchet
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-08-09, by blanchet
fiddle some more with "max_new_relevant_facts_per_iter"
2010-08-09, by blanchet
replace recursion with "fold"
2010-08-09, by blanchet
remove debugging output
2010-08-09, by blanchet
remove now needless "Thm.transfer"
2010-08-09, by blanchet
reintroduced old code that removed axioms from the conjecture assumptions, ported to FOF
2010-08-09, by blanchet
merge
2010-08-09, by blanchet
fix embarrassing bug in elim rule handling, introduced during the port to FOF
2010-08-09, by blanchet
minor doc changes
2010-08-06, by blanchet
modernized some specifications;
2010-08-11, by wenzelm
tuned;
2010-08-11, by wenzelm
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
2010-08-11, by wenzelm
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
2010-08-11, by wenzelm
proper handling of empty text;
2010-08-11, by wenzelm
more uniform XML/YXML string_of_body/string_of_tree;
2010-08-11, by wenzelm
type XML.Body as basic data representation language (Scala version);
2010-08-10, by wenzelm
type XML.body as basic data representation language;
2010-08-10, by wenzelm
renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;
2010-08-10, by wenzelm
added string_bytes convenience;
2010-08-10, by wenzelm
tuned;
2010-08-10, by wenzelm
removed obsolete methods for (ML) commands;
2010-08-10, by wenzelm
prefer Nimbus look and feel on all platforms, instead of the somewhat ugly javax.swing.plaf.metal.MetalLookAndFeel, which presumably is implicit fall-back nonetheless;
2010-08-10, by wenzelm
edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
2010-08-10, by wenzelm
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
2010-08-10, by wenzelm
added Library.thread_actor -- thread as actor;
2010-08-10, by wenzelm
clarified JEDIT_JAVA_OPTIONS vs. JEDIT_SYSTEM_OPTIONS -- discontinued JEDIT_APPLE_PROPERTIES;
2010-08-10, by wenzelm
auto_flush: higher frequency;
2010-08-09, by wenzelm
uniform raw_dump for input/output fifos on Cygwin;
2010-08-09, by wenzelm
more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
2010-08-09, by wenzelm
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
2010-08-09, by wenzelm
tuned comments;
2010-08-09, by wenzelm
merged
2010-08-09, by wenzelm
added Lars Noschinski to isatest report
2010-08-09, by haftmann
merged
2010-08-09, by wenzelm
discontinued separation of `define` and `declare_const`
2010-08-08, by haftmann
unravelled target initialization code
2010-08-08, by haftmann
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
2010-08-08, by boehmes
added scanning of if-then-else expressions
2010-08-08, by boehmes
merged
2010-08-06, by blanchet
added support for partial quotient types;
2010-08-06, by blanchet
adapt occurrences of renamed Nitpick functions
2010-08-06, by blanchet
document the non-legacy interfaces
2010-08-06, by blanchet
local versions of Nitpick.register_xxx functions
2010-08-06, by blanchet
parse_spans: somewhat faster low-level implementation;
2010-08-08, by wenzelm
proper context for Syntax.parse_token;
2010-08-08, by wenzelm
prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
2010-08-08, by wenzelm
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-08-08, by wenzelm
fixed odd runtime type error, which appears to have escaped the scala-2.8.0.final compiler;
2010-08-08, by wenzelm
YXML.parse: refrain from interning, let XML.Cache do it (partially);
2010-08-08, by wenzelm
cache_string: store trimmed string value;
2010-08-08, by wenzelm
simple_dialog: allow scala.swing.Component as well;
2010-08-07, by wenzelm
simplified some Markup;
2010-08-07, by wenzelm
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
2010-08-07, by wenzelm
more robust treatment of Markup.token;
2010-08-07, by wenzelm
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
2010-08-07, by wenzelm
concentrate structural document notions in document.scala;
2010-08-07, by wenzelm
maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
2010-08-07, by wenzelm
tuned;
2010-08-07, by wenzelm
more explicit model of pending text edits;
2010-08-07, by wenzelm
more explicit treatment of Swing thread context;
2010-08-07, by wenzelm
replaced individual Document_Model history by all-inclusive one in Session;
2010-08-07, by wenzelm
misc tuning and clarification;
2010-08-07, by wenzelm
avoid null in Scala;
2010-08-06, by wenzelm
updated keywords;
2010-08-06, by wenzelm
removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
2010-08-06, by wenzelm
merged
2010-08-06, by wenzelm
merged
2010-08-06, by blanchet
quotient types registered as codatatypes are no longer quotient types
2010-08-06, by blanchet
added a friendly warning
2010-08-06, by blanchet
extend the scope of limitation about nonconservative extensions
2010-08-06, by blanchet
improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
2010-08-06, by blanchet
Remove duplicate locale activation code; performance improvement.
2010-08-05, by ballarin
added record field
2010-08-05, by blanchet
added "whack"
2010-08-05, by blanchet
handle "Rep_unit" & Co. gracefully
2010-08-05, by blanchet
added support for "Abs_" and "Rep_" functions on quotient types
2010-08-05, by blanchet
fiddle with specialization etc.
2010-08-05, by blanchet
handle inductive predicates correctly after change in "def" semantics
2010-08-05, by blanchet
don't specialize built-ins or constructors
2010-08-05, by blanchet
more docs
2010-08-05, by blanchet
prevent the expansion of too large definitions -- use equations for these instead
2010-08-05, by blanchet
make nitpick accept "==" for "nitpick_(p)simp"s
2010-08-05, by blanchet
fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
2010-08-05, by blanchet
deal correctly with Pure.conjunction in mono check
2010-08-05, by blanchet
rename internal functions
2010-08-05, by blanchet
remove buggy and needless condition
2010-08-05, by blanchet
renamed internal function
2010-08-05, by blanchet
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
2010-08-04, by blanchet
avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
2010-08-04, by blanchet
improve datatype symmetry breaking;
2010-08-04, by blanchet
merged
2010-08-04, by blanchet
make SML/NJ happy
2010-08-04, by blanchet
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
2010-08-04, by blanchet
tuning
2010-08-03, by blanchet
better "Pretty" handling
2010-08-03, by blanchet
change formula for enumerating scopes
2010-08-03, by blanchet
example tweaking -- also prevents Nitpick_Tests from using more than 1 thread
2010-08-03, by blanchet
speed up Nitpick examples a little bit
2010-08-03, by blanchet
minor changes
2010-08-03, by blanchet
updated example timings
2010-08-03, by blanchet
more helpful message
2010-08-03, by blanchet
also mention gfp
2010-08-03, by blanchet
bump up the max cardinalities, to use up more of the time given to us by the user
2010-08-03, by blanchet
make tracing monotonicity easier
2010-08-03, by blanchet
more documentation, based on email discussions with a user
2010-08-03, by blanchet
make example easier to parse
2010-08-03, by blanchet
clarify attribute documentation
2010-08-03, by blanchet
choose better example
2010-08-03, by blanchet
fix newly introduced bug w.r.t. conditional equations
2010-08-03, by blanchet
document something I explained in an email to a poweruser
2010-08-03, by blanchet
make Nitpick more flexible when parsing (p)simp rules
2010-08-03, by blanchet
fix soundness bug w.r.t. "Suc" with "binary_ints"
2010-08-03, by blanchet
handle free variables even more gracefully;
2010-08-03, by blanchet
optimize local "def"s by treating them as definitions
2010-08-03, by blanchet
careful about which linear inductive predicates should be starred
2010-08-02, by blanchet
help Nitpick
2010-08-02, by blanchet
fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
2010-08-02, by blanchet
prevent generation of needless specialized constants etc.
2010-08-02, by blanchet
optimize generated Kodkod formula
2010-08-02, by blanchet
prefer implication to equality, to be more SAT solver friendly
2010-08-02, by blanchet
minor symmetry breaking for codatatypes like llist
2010-08-02, by blanchet
fix bug with mutually recursive and nested codatatypes
2010-08-02, by blanchet
fix minor bug in sym breaking
2010-08-01, by blanchet
modernized specifications;
2010-08-06, by wenzelm
Document_Model: include token marker here;
2010-08-05, by wenzelm
tuned;
2010-08-05, by wenzelm
misc tuning -- produce reverse_edits at most once (note that foldRight produces a reversed list internally, while recursion is infisible due to small stack vs. large stack frames on JVM);
2010-08-05, by wenzelm
editor mode;
2010-08-05, by wenzelm
Text_Edit.convert/revert;
2010-08-05, by wenzelm
renamed to_current to convert, and from_current to revert;
2010-08-05, by wenzelm
Change.Snapshot: include from_current/to_current here, with precomputed changes;
2010-08-05, by wenzelm
explicit Change.Snapshot and Document.Node;
2010-08-05, by wenzelm
simplified/refined document model: collection of named nodes, without proper dependencies yet;
2010-08-05, by wenzelm
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
2010-08-05, by wenzelm
uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);
2010-08-04, by wenzelm
load_thy/after_load: explicit check of parent theories, which might have failed to join proofs -- avoid uninformative crash via Graph.UNDEF;
2010-08-04, by wenzelm
export use_thys_wrt;
2010-08-04, by wenzelm
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
2010-08-04, by wenzelm
updated to Netbeans 6.9;
2010-08-04, by wenzelm
schedule_futures: discontinued special treatment of non-parallel proofs, which might have affected memory usage at some point, but does not seem to make a difference with as little as 2GB RAM;
2010-08-04, by wenzelm
more precise CRITICAL sections;
2010-08-03, by wenzelm
removed unused Update_Time data (cf. ac94ff28e9e1);
2010-08-03, by wenzelm
modernized specifications;
2010-08-03, by wenzelm
eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;
2010-08-03, by wenzelm
find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
2010-08-03, by wenzelm
renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
2010-08-03, by wenzelm
tuned headers -- more precise load path;
2010-08-03, by wenzelm
theory loading: only the master source file is looked-up in the implicit load path;
2010-08-03, by wenzelm
load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;
2010-08-03, by wenzelm
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
2010-08-03, by wenzelm
only test prolog code examples if environment variable is set
2010-08-03, by bulwahn