move stuff from Domain.thy to Domain_Aux.thy

move map functions to new theory file Map_Functions; add theory file Plain_HOLCF

allow unpointed lazy arguments for definitional domain package

add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas

merged

removed unused lemma chain_mono2

rename class 'bifinite' to 'domain'

instance sum :: (predomain, predomain) predomain

configure sum type for fixrec

add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)

instance prod :: (predomain, predomain) predomain

adapt isodefl proof script to unpointed types

add 'predomain' class: unpointed version of bifinite

add bifiniteness check for domain_isomorphism command

implement map_of_typ using Pattern.rewrite_term

avoid using stale theory

implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data

add function the_sort

refactor tmp_thy code

reorganize Bifinite.thy; simplify some proofs related to bifinite class instances

treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;

Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;

more precise treatment of deleted nodes;

tuned error message;

unified type Document.Edit;

replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes; Document_Model.pending_edits: more robust treatment of init, including buffer reload event (jEdit 4.3.2 produces malformed remove/insert that lacks the last character); tuned;

tuned;

reduced danger of line breaks within minipage;

Sidekick block asset: show first line only;

added buffer_text convenience, with explicit locking;

use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading);

merged

make SML/NJ happy

merged

slightly changed fun_map_def

fun_rel_def is no simp rule by default

more appropriate specification packages; fun_rel_def is no simp rule by default

type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions

more appropriate specification packages; fun_rel_def is no simp rule by default

type annotations in specifications; fun_rel_def is no simp rule by default

fun_rel_def is no simp rule by default

merged

tidied using metis

manage folding via sidekick by default;

eliminated obsolete heading category -- superseded by heading_level;

treat main theory commands like headings, and nest anything else inside;

proper treatment of equal heading level;

added missing Keyword.THY_SCHEMATIC_GOAL; more keyword categories;

default Sidekick parser based on section headings;

some support for nested source structure, based on section headings;

tuned;

misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);

updated version;

private counter, to keep externalized ids a bit smaller;

added general Synchronized.counter convenience;

explicitly identify forked/joined tasks;

accomodate old manuals that include pdfsetup.sty without isabelle.sty;

merged

removed type-inference-like behaviour from relation_tac completely; tuned

avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);

explicitly check uniqueness of symbol recoding;

more hints on building and running Isabelle/jEdit from command line;

merged

merge

reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving

merged

merged

(infixl "<<" 55) -> (infix "<<" 50)

simplify some proofs

remove unnecessary stuff from Discrete.thy

remove some unnecessary lemmas; move monofun_LAM to Cfun.thy

add lemma eq_imp_below

discontinue a bunch of legacy theorem names

move a few admissibility lemmas into FOCUS/Stream_adm.thy

simplify some proofs

compile -- 7550b2cba1cb broke the build

merge

recognize Vampire error

return the process return code along with the process outputs

better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)

merged

corrected slip: must keep constant map, not type map; tuned code

constructors to datatypes in code_reflect can be globbed; dropped unused code

adding code and theory for smallvalue generators, but do not setup the interpretation yet

make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice

better detection of completely irrelevant facts

always use a hard timeout in Mirabelle

use "smt" (rather than "metis") to reconstruct SMT proofs

don't pass too many facts on the first iteration of the SMT solver

catch TimeOut exception

ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns

if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed

removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway

make Nitpick datatype tests faster to make timeout less likely

invoke SMT solver in a loop, with fewer and fewer facts, in case of error

always honor the max relevant constraint