functional theory setup -- requires linear access;

simplified print_simpset;

purely functional setup of claset/simpset/clasimpset; tuned signature;

purely functional setup of claset/simpset/clasimpset;

fixed spelling;

added exec_file; tuned;

CRITICAL: further trace levels for 1000ms and 100ms;

removed obsolete store_thm(s), cf. functional versions in pure_thy.ML; tuned;

added generic_theory transaction;

commands 'use' and 'ML' now thy_decl; removed obsolete 'ML_setup' -- superceded by 'ML';

removed obsolete use_XXX; added ml_diag;

eliminated destructive/critical theorem database; simplified store_thm(s); removed obsolete smart_store_thm(s); tuned;

certify wrt. dynamic context; functional store_thm (wrt. thread data);

added map_theory_result, map_proof_result;

certify wrt. dynamic context;

eliminated non-linear access to thy1 and thy12c;

replaced 'ML' by diagnostic 'ML_command';

updated generated file;

simplified PureThy.store_thm;

replaced 'ML_setup' by 'ML';

* Eliminated destructive theorem database. * Commands 'use' and 'ML' are now purely functional; added diagnostic 'ML_val'.

eliminated quiete_mode ref (not really needed);

eliminated quiete_mode ref (turned into proper argument);

eliminated quiete_mode ref (unused);

eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);

added forget_structure;

eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;

ml_tactic: non-critical version via proof data and thread data;

NAMED_CRITICAL;

unfold_locales now part of default tactic

import Main explicitly

dropped now superfluous ad-hoc adaption

not depends on Main any longer

accomodated to sledgehammer theory dependency requirement

only invoke interpret

updated generated file;

Context.>> : operate on Context.generic;

avoid rebinding of existing facts;

some styling

some styling

some styling

tuned proofs

tuned;

updated dependencies;

reorganized signature of ML_Context;

remove commented text

avoid ambiguity of State.state vs. JVMType.state;

declare cont_lemmas_ext as simp rules individually

avoid amiguity of Continuity.chain vs. Porder.chain;

avoid amiguity of State.state vs. JVMType.state;

changed wrong assignement in signature sections

clarified character serializations

added Enum

circumventing merge problem

explicit case names for rule list_induct2

instance for functions, explicit characters

lemmas about map_of (zip _ _)

restructuring; explicit case names for rule list_induct2

no "attach UNIV" any more

tuned comments; tuned;

tuned comments;

fixed theory imports;

tuned appendix;

removed obsolete appl_syntax, applC_syntax;

eliminated delayed theory setup

Command 'setup': discontinued implicit version.

eliminated theory ProtoPure; renamed ML_Context.the_context to ML_Context.the_global_context;

renamed ML_Context.the_context to ML_Context.the_global_context; moved old the_context to old_goals.ML;

added process_file;

eliminated theory ProtoPure; implicit setup of emerging theory Pure;

moved old the_context here; eliminated theory ProtoPure; renamed ML_Context.the_context to ML_Context.the_global_context;

eliminated theory ProtoPure; implicit setup of emerging theory Pure; added >>> operator;

implicit setup of emerging theory Pure;

reduced to theory body (cf. OuterSyntax.process_file);

renamed ML_Context.the_context to ML_Context.the_global_context;

eliminated theory ProtoPure;

removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);

HOL (and FOL): renamed variables in rules imp_elim and swap; Eliminated theory ProtoPure.

nonfix >>;

make preorder locale into a superclass of class po

removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);

removed legacy ML bindings;

rule swap: renamed Pa to P;

added store_thms etc. (formerly in Thy/thm_database.ML); added bind_thm(s) (formerly in old_goals.ML); adapted to Context.thread_data interface; removed obsolete get/set_context; renamed ML_Context.>> to Context.>> (again);

adapted to Context.thread_data interface;

moved bind_thm(s) to ML/ml_context.ML; removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);

added thread data (formerly global ref in ML/ml_context.ML); renamed ML_Context.>> to Context.>> (again);

pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;

pass imp_elim, swap to classical prover;

updated generated file;

renamed ML_Context.>> to Context.>> (again);

converted legacy ML scripts;

rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite

fix spelling errors

removed obsolete pass, save;

use_thy: removed obsolete ML_Context.save;

removed obsolete use_thy (cf. isar_syn.ML);

use poly-cvs as name

Functor NamedThmsFun: data is available to the user as dynamic fact;

update_context: always store as "Nominal.eqvts"; added dynamic fact bindings for "eqvts", "freshs", "bijs";

added command 'ML_val' (presently just a clone of 'ML');

removed redundant axiomatizations of XXX_infinite (fact already proven);

add dynamic fact binding;

added 'ML_val' command (diagnostic);

get fact: do not compare names;

*** empty log message ***

support dynamic facts;

setup for dynamic "prems" (legacy);

more antiquotations;

moved multithreaded "profile" to multithreading_polyml.ML;

use polyml_old_compiler5.ML;

removed

removed obsolete use_legacy_bindings;

ML runtime compilation: pass position, tuned signature; removed obsolete (use_)legacy_bindings;

ML runtime compilation: pass position, tuned signature;

removed junk;

Runtime compilation -- for old version of PolyML.compilerEx (version 5.0, 5.1).

Runtime compilation -- for old version of PolyML.compiler (version 4.x).

Compatibility wrapper for Poly/ML 5.1.

removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1); moved use_text/file to polyml_old_compiler4.ML; PolyML.onEntry: no longer evaluate command line;