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.