merged

Got rid of a warning about duplicate rewrite rules.

accumulate only local results -- no proper history support yet;

avoid deprecated Iterator.fromArray;

more compiler warnings;

eliminated hard tabs;

assume given SCALA_HOME, e.g. from component settings or external setup;

merged

merged

make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work

Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes

make Nitpick "show_all" option behave less surprisingly

merged

avoid reference to thm PairE

more coherent theory structure; tuned headings

made SML/NJ quite happy;

reuse main view.font from jEdit;

deleted some old fonts;

also set font for printing, which actually works out of the box;

lib/Tools/makeall does not hardiwre logics;

discontinued Sun/Solaris tests;

some updates for release;

merged

added function update examples and set examples

updated SMT certificates

sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)

merged

renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")

made script executable

use Z3's builtin support for div and mod

moved SMT into the HOL image

slightly odd workaround to ignore markup that is typically displaced;

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; tuned;

further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;

renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;

misc updates for release;

constant Rat.normalize needs to be qualified;

merged

merged

dropped legacy theorem bindings

dropped legacy theorem bindings

dropped legacy theorem bindings

dropped legacy theorem bindings

dropped legacy theorem bindings

normalized references to constant "split"

Revise locale test theory layout.

Merge mixins of distinct interpretations with same base.

indicate prospective properties;

clarified auto_update vs. update; tuned;

more reactive message handling, notably for follow_caret mode; misc tuning and clarification;

Command.toString: include id for debugging; Command.consume: explicit forward, avoid dependency on Session and side-effect on event bus; State.+ without side-effect on event bus; Session.commands_changed: delayed command changes (outside of Swing thread), also subsumes former Session.results; Document_View: tuned commands_changed handling and caret listening; Document_View.selected_command: proper function, not event handler state; Output_Dockable: directly act upon commands_changed, not caret events (via former Session.results);

merged

refer to polyml-5.3.0-old for ppc-darwin;

try logical and theory abstraction before full abstraction (avoids warnings of linarith)

updated SMT certificates

hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns

more convenient order of code equations

misc updates for release;

eliminated obsolete priority message from Isabelle_Process protocol;

moved ML files where they are actually used; more precise dependencies;

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;

eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;

eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;

tuned -- avoid catch-all exception pattern;

updated generated files;

merged

merged

Typo fixed.

move HOLCF/Sum_Cpo.thy to HOLCF/Library

move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path

move unused pattern match syntax stuff into HOLCF/ex

rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed

more lemmas

induction and case rules

Store registrations in efficient data structure.

Avoid recomputation of registration instance for lookup.

Consistently use equality for registration lookup.

Cleaner implementation of sublocale command.

Reapply mixin patch: base for performance improvements.

merged

declare a few more cont2cont rules

HOLCF no longer redefines 'consts' command

for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run

simplify fixrec continuity tactic

used sledgehammer[isar_proof] to replace slow metis call

Typo fixed.

Typo fixed.

Minor proof tuning.

Improved document structure.

Minor proof tuning.

merged

Refactoring, minor extensions (e.g., church_rosser).

NEWS: removed fixrec_simp attribute

merged

disambiguate some syntax

optimize continuity proofs in fixrec package, using cont2cont rules

add beta_cfun simproc, which uses cont2cont rules

removed fixrec_simp attribute (cf. a2a1c8a658ef)

simplify definition of eta_tac

remove fixrec_simp attribute; fixrec uses default simpset from theory context instead

remove cont2cont simproc; instead declare cont2cont rules as simp rules

domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context

merged

modernized sorting algorithms; quicksort implements sort

modernized sorting algorithms; quicksort implements sort

localized properties_for_sort

@tailrec annotation;

renamed "rev" to "reverse" following usual Scala conventions;

parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;

added rev_iterator;

tuned;

access statically typed dockable windows;

simplified dockables using class Dockable;

generic dockable window;

separate event bus and dockable for raw output (stdout);

more Mac OS problems;

ignore system messages;

use proper ISABELLE_PLATFORM instead of adhoc uname;

refrain from using bold within the term language -- looks odd in Lobo with error/warning background;