merged

merged

merged

fixed proof (cf. a81f95693c68);

tuned Isar output

tuned

updated docs

renamed Isar-proof related options + changed semantics of Isar shrinking

tuning

fixed theorem lookup code in Isar proof reconstruction

tuning

refactor code

tuning

more robust future_proof result with specific error message (e.g. relevant for incomplete proof of non-registered theorem);

collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);

more uniform group for map_future, which is relevant for cancel in worker_task vs. future_job -- prefer peer group despite 81d03a29980c;

tuned message;

tuned comment;

avoid spurious "bad" markup for show/test_proof; tuned;

more official Future.terminate; tuned signature;

simp results for simplification results of Inf/Sup expressions on bool; tuned proofs

no sort constraints on datatype constructors in internal bookkeeping

HOL-BNF-Examples is sequential for now, due to spurious interrupts (again);

merged

comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic

checking for bound variables in the set expression; handling negation more generally

set_comprehension_pointfree simproc now handles the complicated test case; tuned

refined conversion to only react on proper set comprehensions; tuned

moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)

employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc

another Future.shutdown after Future.cancel_groups (cf. 0d4106850eb2);

more robust cancel_now: avoid shooting yourself in the foot;

more robust Session.finish (batch mode): use Goal.finish_futures to exhibit remaining failures of disconnected goal forks (e.g. from unnamed theorems) and Goal.cancel_futures the purge the persistent state;

proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;

added Output "Detach" button;

skipped proofs appear as "bad" without counting as error;

more method position information, notably finished_pos after end of previous text;

more formal markup;

tuned signature; prefer exception Fail for internal errors;

more formal markup;

don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule

merged

added missing file

tuned for document output

added proof minimization code from Steffen Smolka

tuned blank lines

tuned whitespace

a few notations changed in HOL/BNF/Examples/Derivation_Trees

ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package

adding test cases for f x y : S patterns in set_comprehension_pointfree simproc

tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage

term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage

extending preprocessing of simproc to rewrite subset inequality into membership of powerset

update ROOT with teh directory change in BNF

changed name of BNF/Example directory from Infinite_Derivation_Trees to Derivation_Trees

retain info dockable state via educated guess on window focus;

support for more informative errors in lazy enumerations;

more informative errors for 'also' and 'finally';

tuned messages;

more proof method text position information;