isabelle: Graph

discontinued support for Poly/ML 5.0 and 5.1 versions;
2010-08-17, by wenzelm
updated for prospective Poly/ML 5.4;
2010-08-17, by wenzelm
multi-platform build script for Poly/ML;
2010-08-17, by wenzelm
updated keywords;
2010-08-17, by wenzelm
updated Named_Target.init;
2010-08-17, by wenzelm
made 9043eefe8d71 actually compile;
2010-08-17, by wenzelm
merged
2010-08-17, by wenzelm
merged
2010-08-17, by haftmann
formally document `code abstype` and `code abstract` attributes
2010-08-17, by haftmann
NEWS and CONTRIBUTORS
2010-08-17, by haftmann
nicer code for rev
2010-08-17, by haftmann
reworked section on simple datatype refinement
2010-08-17, by haftmann
tuned whitespace
2010-08-17, by haftmann
merged
2010-08-17, by blanchet
typos in comment
2010-08-16, by blanchet
more debug output
2010-08-16, by blanchet
detect old Vampire and give a nicer error message
2010-08-16, by blanchet
merged
2010-08-17, by nipkow
now works for schematic terms as well, thanks to Alex for the `how-to'
2010-08-17, by nipkow
added section on program refinement
2010-08-17, by haftmann
tuned whitespace
2010-08-17, by haftmann
tune;
2010-08-17, by wenzelm
added functor Linear_Set, based on former adhoc structures in document.ML;
2010-08-17, by wenzelm
HOL-Proofs-Extraction: some workaround to make it work in low-memory situations (e.g. atbroy102 with as little as 1GB heap space);
2010-08-16, by wenzelm
XML.Cache: pipe-lined (thread-safe) version using actor;
2010-08-16, by wenzelm
simplified internal message format: dropped special Symbol.STX header;
2010-08-16, by wenzelm
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
2010-08-16, by wenzelm
merged
2010-08-16, by wenzelm
merged
2010-08-16, by haftmann
tuned section on predicate compiler
2010-08-16, by haftmann
section "if something goes utterly wrong"
2010-08-16, by haftmann
merged
2010-08-16, by haftmann
merged
2010-08-16, by haftmann
adaptation to new outline
2010-08-16, by haftmann
merged
2010-08-13, by haftmann
corrected handling of `constrains` elements
2010-08-13, by haftmann
removed non-BSD compatible option from cp
2010-08-16, by kleing
Geoff's formatter now needs closed formulas
2010-08-16, by blanchet
Using type real does not require a separate logic now.
2010-08-15, by nipkow
merged
2010-08-15, by nipkow
tuned text about "value" and added note on comments.
2010-08-15, by nipkow
simplified command status: interpret stacked markup on demand;
2010-08-16, by wenzelm
event_bus.scala rather belongs to system plumbing;
2010-08-15, by wenzelm
some derived operations on Text.Range;
2010-08-15, by wenzelm
specific types Text.Offset and Text.Range;
2010-08-15, by wenzelm
moved Text_Edit to Text.Edit;
2010-08-15, by wenzelm
moved History/Snapshot to document.scala;
2010-08-15, by wenzelm
renamed raw_results to raw_protocol;
2010-08-15, by wenzelm
rename "unit" to "atom", to avoid confusion with the unit type;
2010-08-15, by wenzelm
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
2010-08-15, by wenzelm
use Synchronized.var and prevent global CRITICAL sections in this hot spot;
2010-08-15, by wenzelm
renamed create_id to new_id;
2010-08-15, by wenzelm
more explicit / functional ML version of document model;
2010-08-15, by wenzelm
renamed class Document to Document.Version etc.;
2010-08-15, by wenzelm
fixed Isabelle/Scala build (cf. f3220ef79d51);
2010-08-15, by wenzelm
Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
2010-08-14, by wenzelm
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
2010-08-14, by wenzelm
Keyword.status: always suppress position;
2010-08-14, by wenzelm
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
2010-08-14, by wenzelm
merged
2010-08-14, by wenzelm
robustified proof
2010-08-13, by haftmann
lemma execute_bind_case
2010-08-13, by haftmann
unit and bool are instances of heap
2010-08-13, by haftmann
merged
2010-08-13, by haftmann
sketch of new outline
2010-08-13, by haftmann
sketch of new outline
2010-08-13, by haftmann
ditem
2010-08-13, by haftmann
refined abstract
2010-08-13, by haftmann
added stub "If something utterly fails"
2010-08-13, by haftmann
avoid variable name acc (cf. cs. 3142c1e21a0e)
2010-08-13, by haftmann
import swap prevents strange failure of SML code generator for datatypes
2010-08-13, by haftmann
added setup
2010-08-13, by haftmann
merged
2010-08-12, by haftmann
group record-related ML files
2010-08-12, by haftmann
merged
2010-08-12, by haftmann
dropped dead code
2010-08-12, by haftmann
moved Record.thy from session Plain to Main; avoid variable name acc
2010-08-12, by haftmann
group record-related ML files
2010-08-12, by haftmann
Class.declare -> Class.const
2010-08-12, by haftmann
named target is optional; explicit Name_Target.reinit
2010-08-12, by haftmann
named target is optional
2010-08-12, by haftmann
Named_Target.init: empty string represents theory target
2010-08-12, by haftmann
Named_Target.theory_init
2010-08-12, by haftmann
simplified code
2010-08-12, by Christian Urban
tuned
2010-08-12, by haftmann
tuned
2010-08-12, by haftmann
merged
2010-08-11, by haftmann
tuned whitespace
2010-08-11, by haftmann
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