isabelle: Graph

merged
2010-06-01, by haftmann
corrected printing of characters
2010-06-01, by haftmann
corrected implementation
2010-06-01, by haftmann
added Scala code setup
2010-06-01, by haftmann
tuned code setup
2010-06-01, by haftmann
keep structure ThyLoad for the sake of Proof General;
2010-06-01, by wenzelm
added random instance for word
2010-06-01, by haftmann
notes on Isabelle/jEdit;
2010-05-31, by wenzelm
remove presently unused Isabelle application;
2010-05-31, by wenzelm
modernized some structure names, keeping a few legacy aliases;
2010-05-31, by wenzelm
merged
2010-05-31, by wenzelm
merge
2010-05-31, by blanchet
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
2010-05-31, by blanchet
updated generated files
2010-05-31, by haftmann
clarified
2010-05-31, by haftmann
adjusted
2010-05-31, by haftmann
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
2010-05-31, by wenzelm
Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;
2010-05-31, by wenzelm
merged
2010-05-31, by wenzelm
Typo in locales tutorial.
2010-05-30, by ballarin
Theory_Target.pretty: more markup;
2010-05-31, by wenzelm
tuned abbrevs for long arrows, according to usual ASCII syntax;
2010-05-31, by wenzelm
more flexibile font size via CSS <style> instead of old <font> element;
2010-05-31, by wenzelm
tuned;
2010-05-31, by wenzelm
control tooltip font via Swing HTML, with tooltip-font-size property;
2010-05-30, by wenzelm
added HTML.encode (in Scala), similar to HTML.output in ML;
2010-05-30, by wenzelm
one extra space to accomodate symbolic indentifiers etc.;
2010-05-30, by wenzelm
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
2010-05-30, by wenzelm
more detailed token markup, including command kind as sub_kind;
2010-05-30, by wenzelm
tuned;
2010-05-30, by wenzelm
separate markup for ML delimiters;
2010-05-30, by wenzelm
less pschedelic token markup;
2010-05-30, by wenzelm
simplified command/keyword markup;
2010-05-30, by wenzelm
markup non-identifier keyword as operator;
2010-05-30, by wenzelm
Isabelle_Process: do not enforce future_terminal_proof by default -- no error propagation yet;
2010-05-30, by wenzelm
more basic default behaviour of ENTER, HOME, END;
2010-05-30, by wenzelm
tuned messages;
2010-05-29, by wenzelm
do not highlight ignored command spans;
2010-05-29, by wenzelm
more explicit handling of document;
2010-05-29, by wenzelm
explicit markup for forked goals, as indicated by Goal.fork;
2010-05-29, by wenzelm
avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;
2010-05-29, by wenzelm
define_state/new_state: provide state immediately, which is now lazy;
2010-05-29, by wenzelm
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
2010-05-29, by wenzelm
future result: retain plain Interrupt for vacuous group exceptions;
2010-05-29, by wenzelm
remove two examples, now that the definition of "fst" and "snd" has changed
2010-05-28, by blanchet
merged
2010-05-28, by wenzelm
Got rid of a warning about duplicate rewrite rules.
2010-05-28, by webertj
accumulate only local results -- no proper history support yet;
2010-05-28, by wenzelm
avoid deprecated Iterator.fromArray;
2010-05-28, by wenzelm
more compiler warnings;
2010-05-28, by wenzelm
eliminated hard tabs;
2010-05-28, by wenzelm
assume given SCALA_HOME, e.g. from component settings or external setup;
2010-05-28, by wenzelm
merged
2010-05-28, by wenzelm
merged
2010-05-28, by blanchet
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-28, by blanchet
Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes
2010-05-27, by blanchet
make Nitpick "show_all" option behave less surprisingly
2010-05-27, by blanchet
merged
2010-05-28, by haftmann
avoid reference to thm PairE
2010-05-28, by haftmann
more coherent theory structure; tuned headings
2010-05-28, by haftmann
made SML/NJ quite happy;
2010-05-28, by wenzelm
reuse main view.font from jEdit;
2010-05-28, by wenzelm
deleted some old fonts;
2010-05-28, by wenzelm
also set font for printing, which actually works out of the box;
2010-05-28, by wenzelm
lib/Tools/makeall does not hardiwre logics;
2010-05-28, by wenzelm
discontinued Sun/Solaris tests;
2010-05-28, by wenzelm
some updates for release;
2010-05-28, by wenzelm
merged
2010-05-27, by wenzelm
added function update examples and set examples
2010-05-27, by boehmes
updated SMT certificates
2010-05-27, by boehmes
sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
2010-05-27, by boehmes
merged
2010-05-27, by boehmes
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
2010-05-27, by boehmes
made script executable
2010-05-27, by boehmes
use Z3's builtin support for div and mod
2010-05-27, by boehmes
moved SMT into the HOL image
2010-05-27, by boehmes
slightly odd workaround to ignore markup that is typically displaced;
2010-05-27, by wenzelm
substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
2010-05-27, by wenzelm
further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
2010-05-27, by wenzelm
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27, by wenzelm
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-27, by wenzelm
misc updates for release;
2010-05-27, by wenzelm
constant Rat.normalize needs to be qualified;
2010-05-27, by wenzelm
merged
2010-05-27, by wenzelm
merged
2010-05-27, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
normalized references to constant "split"
2010-05-26, by haftmann
Revise locale test theory layout.
2010-05-26, by ballarin
Merge mixins of distinct interpretations with same base.
2010-05-26, by ballarin
indicate prospective properties;
2010-05-27, by wenzelm
clarified auto_update vs. update;
2010-05-27, by wenzelm
more reactive message handling, notably for follow_caret mode;
2010-05-27, by wenzelm
Command.toString: include id for debugging;
2010-05-27, by wenzelm
merged
2010-05-26, by wenzelm
refer to polyml-5.3.0-old for ppc-darwin;
2010-05-26, by wenzelm
try logical and theory abstraction before full abstraction (avoids warnings of linarith)
2010-05-26, by boehmes
updated SMT certificates
2010-05-26, by boehmes
hide constants and types introduced by SMT,
2010-05-26, by boehmes
more convenient order of code equations
2010-05-26, by haftmann
misc updates for release;
2010-05-26, by wenzelm
eliminated obsolete priority message from Isabelle_Process protocol;
2010-05-25, by wenzelm
moved ML files where they are actually used;
2010-05-25, by wenzelm
renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;
2010-05-25, by wenzelm
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
2010-05-25, by wenzelm
eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
2010-05-25, by wenzelm
tuned -- avoid catch-all exception pattern;
2010-05-25, by wenzelm
updated generated files;
2010-05-25, by wenzelm
merged
2010-05-25, by wenzelm
merged
2010-05-24, by webertj
Typo fixed.
2010-05-24, by webertj
move HOLCF/Sum_Cpo.thy to HOLCF/Library
2010-05-24, by huffman
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
2010-05-24, by huffman
move unused pattern match syntax stuff into HOLCF/ex
2010-05-24, by huffman
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
2010-05-24, by huffman
more lemmas
2010-05-24, by haftmann
induction and case rules
2010-05-24, by haftmann
Store registrations in efficient data structure.
2010-05-24, by ballarin
Avoid recomputation of registration instance for lookup.
2010-05-24, by ballarin
Consistently use equality for registration lookup.
2010-05-24, by ballarin
Cleaner implementation of sublocale command.
2010-05-24, by ballarin
Reapply mixin patch: base for performance improvements.
2010-05-24, by ballarin
merged
2010-05-23, by huffman
declare a few more cont2cont rules
2010-05-23, by huffman
HOLCF no longer redefines 'consts' command
2010-05-22, by huffman
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
2010-05-22, by huffman
simplify fixrec continuity tactic
2010-05-22, by huffman
used sledgehammer[isar_proof] to replace slow metis call
2010-05-23, by krauss
Typo fixed.
2010-05-23, by webertj
Typo fixed.
2010-05-23, by webertj
Minor proof tuning.
2010-05-23, by webertj
Improved document structure.
2010-05-23, by webertj
Minor proof tuning.
2010-05-23, by webertj
merged
2010-05-23, by webertj
Refactoring, minor extensions (e.g., church_rosser).
2010-05-23, by webertj
NEWS: removed fixrec_simp attribute
2010-05-22, by huffman
merged
2010-05-22, by huffman
disambiguate some syntax
2010-05-22, by huffman
optimize continuity proofs in fixrec package, using cont2cont rules
2010-05-22, by huffman
add beta_cfun simproc, which uses cont2cont rules
2010-05-22, by huffman
removed fixrec_simp attribute (cf. a2a1c8a658ef)
2010-05-22, by huffman
simplify definition of eta_tac
2010-05-22, by huffman
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
2010-05-22, by huffman
remove cont2cont simproc; instead declare cont2cont rules as simp rules
2010-05-22, by huffman
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
2010-05-22, by huffman
merged
2010-05-22, by haftmann
modernized sorting algorithms; quicksort implements sort
2010-05-22, by haftmann
modernized sorting algorithms; quicksort implements sort
2010-05-22, by haftmann
localized properties_for_sort
2010-05-22, by haftmann
@tailrec annotation;
2010-05-24, by wenzelm
renamed "rev" to "reverse" following usual Scala conventions;
2010-05-24, by wenzelm
parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;
2010-05-22, by wenzelm
added rev_iterator;
2010-05-22, by wenzelm
tuned;
2010-05-22, by wenzelm
access statically typed dockable windows;
2010-05-22, by wenzelm
simplified dockables using class Dockable;
2010-05-22, by wenzelm
generic dockable window;
2010-05-22, by wenzelm
separate event bus and dockable for raw output (stdout);
2010-05-22, by wenzelm
more Mac OS problems;
2010-05-22, by wenzelm
ignore system messages;
2010-05-22, by wenzelm
use proper ISABELLE_PLATFORM instead of adhoc uname;
2010-05-22, by wenzelm
refrain from using bold within the term language -- looks odd in Lobo with error/warning background;
2010-05-22, by wenzelm
tuned;
2010-05-22, by wenzelm
removed timing;
2010-05-22, by wenzelm
rendering information and style sheets via settings;
2010-05-22, by wenzelm
more brackets -- unaligned to prevent odd auto-indentation;
2010-05-21, by wenzelm
merged
2010-05-21, by wenzelm
adjusted to changes in Mapping.thy
2010-05-21, by haftmann
merged
2010-05-21, by haftmann
tuned
2010-05-21, by haftmann
more lemmas about mappings, in particular keys
2010-05-21, by haftmann
refined
2010-05-21, by haftmann
nats in Haskell are readable
2010-05-21, by haftmann
Let rsp and prs in fun_rel/fun_map format
2010-05-21, by Cezary Kaliszyk
tuned zoom_box;
2010-05-21, by wenzelm
print calculation result in the context where the fact is actually defined -- proper externing;
2010-05-21, by wenzelm
future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);
2010-05-21, by wenzelm
some message styling;
2010-05-21, by wenzelm
simplified message markup, using plain XML.Elem directly;
2010-05-21, by wenzelm
more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
2010-05-21, by wenzelm
refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;
2010-05-21, by wenzelm
bad_result: report fully explicit message;
2010-05-21, by wenzelm
observe additional isabelle-jedit.css for component and user;
2010-05-21, by wenzelm
added checkboxes for debug/tracing filter;
2010-05-21, by wenzelm
more abstract view on prover output messages;
2010-05-21, by wenzelm
added some tooltips;
2010-05-21, by wenzelm
HTML_Panel.handler as overridable method;
2010-05-21, by wenzelm
added Library.undefined (in Scala);
2010-05-21, by wenzelm
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
2010-05-21, by wenzelm