isabelle: Graph

tuned internal structure
2010-08-11, by haftmann
remove reinit operation alltogether
2010-08-11, by haftmann
avoid arcane Local_Theory.reinit entirely
2010-08-11, by haftmann
more convenient split of class modules: class and class_declaration
2010-08-11, by haftmann
tuned
2010-08-11, by haftmann
stripped signature
2010-08-11, by haftmann
explicit accessed to structure Class_Target
2010-08-11, by haftmann
tuned lowercase
2010-08-11, by haftmann
moved Document.text_edits to Thy_Syntax;
2010-08-14, by wenzelm
tuned;
2010-08-14, by wenzelm
added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);
2010-08-13, by wenzelm
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