isabelle: Graph

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