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