merged

dedicated exec ... syntax for open state monad (partly already introduces in d00a3f47b607)

merged

more generous memory settings for scala check

no polymorphic "var"s

merged

adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples

do a better job at Skolemizing in Nitpick, for TPTP FOF

revert code that was submitted by mistake

renamings + only need second component of name pool to reconstruct proofs

rename "classrel" to "class_rel"

rename "combtyp" constructors

renamed "Literal" to "FOLLiteral"

renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators

merged

fixing quickcheck invocation in HOL-Mirabelle

hiding constants in Quickcheck_Types

adding a type for flat complete lattice to Quickcheck_Types

added new theories to IsaMakefile and ROOT.ML

adding Quickcheck examples for other quickcheck default types

adding Library theory for other quickcheck default types

removing obsolete ID in Quickcheck_Examples

correcting wellsortedness check and improving error message

using multiple default types in quickcheck

correcting merging of default_types

reordering quickcheck signature; exporting test_params and inspection function

changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types

putting proof in the right context; adding if rewriting; tuned

load_thy: parallel parsing of units, which consist of statement/proof each;

eliminated some unreferenced identifiers;

tuned;

tuned comments;

replaced Source.of_list_limited by slightly more economic Source.of_string_limited;

deps_thy/load_thy: store compact text to reduce space by factor 12;

make SML/NJ happy, by adhoc type-constraints;

recovered benchmarks, which are not tested automatically;

made SML/NJ happy;

merged

abstract visualization of locale ingredients; all_locales yields proper locale identifiers

tuned

accomodate for scope of "as" binding in ML

tuned code

datatype classes are abstract

avoid deprecation

robustified metis proof

modernized abel_cancel simproc setup

keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup

diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq

diff_minus subsumes diff_def

tuned whitespace

dropped essentially ineffective tuning

discontinued pretending that abel_cancel is logic-independent; cleaned up junk

merged

merged

distinguish different classes of const syntax

Scala: subtle difference in printing strings vs. complex mixfix syntax

check code generation for Scala

dropped superfluous prefixes

optional break

consolidate const_syntax naming

recovered benchmarks, which are not tested automatically;

reactivate SML/NJ test on macbroy28, while macbroy23 is unavailable;

eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing; misc tuning and simplification;

moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;

replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;

thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;

explicit dependency on theory HOL;

ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state; recovered @{theory_ref NAME} (cf. 1f09a22a1027);

added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);

thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;

clarified/exported Future.worker_subgroup, which is already the default for Future.fork;

qualified Thy_Info.get_theory;

discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;

further Mac OS X deviations;

warning in proper transaction context;

SML/NJ: refrain from modifying toplevel pp for type string -- unclear if it could work here;

avoid duplicate printing of 'theory' state (cf. 173974e07dea);

toplevel pp for Proof.state and Toplevel.state;

execute document version at high priority;

Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;

edit_document: join parent execution in synchronous/uninterruptible mode, to prevent spurious interrupts when cascaded executions run into each other;

back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c); cancel passive tasks more actively via Exn.Interrupt, by treating them like ragular jobs here; attempts to re-assign canceled futures/promises raise Exn.Interrupt; tuned;

export Graph.get_entry for convenience;

eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that; tuned some error messages;

tuned;

observe follow_caret (again);

Session: predefined real time parameters; Document_View: delayed caret handling, for improved reactivity; selected_command: proper_command_at ignores ignored commands;

bind and then latex symbols

minor update of dependencies;

corrected range chec

first roughly working version of Imperative HOL for Scala

tuned

merged

a first sketch for Imperative HOL witht Scala

don't fail gracefully

restored long-broken syntax sanity checks

tuned interpunctation

fragments of Scala

merged

adjusted; fixed typo

dropped spurious export_code

use different log server (macbroy23 down)

more consistent spacing in generated monadic code

braced needed in layout-insensitive syntax

repaired some implementations of imperative operations

repaired reference implementation for OCaml

part of pervasive test

avoid ambiguities; tuned

repaired of_list implementation for SML, OCaml

avoid export_code ... file -

explicit optional checking

added Isar syntax for code checking

corrected import

use generic description slot for formal code checking

formal slot for code checker

export_code without file prints to standard output

check without explicit path

load cache_io before code generator; moved adhoc-overloading to generic tools

tuned infix syntax

dropped M suffix; added predicate monad bind