avoid rebinding of existing facts;

removed duplicate lemmas;

only one version of group.rcos_self;

Facts.add_local;

Facts.add_global;

replaced generic add by add_local/add_global; add_global: report/ignore duplicate bindings;

proper naming of weak_ref_map2ref_map;

avoid rebinding of existing facts; proper ML antiquotations;

avoid rebinding of existing facts;

added Compl_Collect;

proper naming of knows_Outpts_insecureM, knows_subset_knows_A_Gets;

renamed K3_imp_Gets variant to K3_imp_Gets_evs;

removed duplicate lemmas;

closeup: recover original order of free variables!

reorganization

added lemmas

remove unneeded constant mod_alt

More defns and thms

fixed broken bintrunc lemma

tuned;

get_thm(s): check facts lookup vs. old thm database;

tuned messages;

del: hide in name space;

avoid unclear fact references;

eliminated out-of-scope proofs (cf. theory IFOL and FOL); proper antiquotations;

proper antiquotations;

added lemmas from simpdata.ML;

removed obsolete PureThy.thms_containing;

replaced obsolete FactIndex.T by Facts.T; removed unused get_thm(s)_closure; removed obsolete theorems_of, fact_index_of, lthms_containing, hide_thms;

more precise Author line; replaced obsolete FactIndex.T by Facts.T; simplified ML;

replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories); removed unused get_thm(s)_closure; removed obsolete fact_index_of, valid_thms, thms_containing(_consts);

Environment of named facts (admits overriding). Optional indexing by proposition.

obsolete (cf. facts.ML);

removed obsolete fact_index.ML; added facts.ML;

replaced obsolete FactIndex.T by Facts.T;

removed obsolete PureThy.thms_containing_consts;

explicit re-init

(continued)

continued localization

Orders as relations

Added Order_Relation

Added lemmas

restore instead of init

restore replaces reinit

added mk_const functions

added combinator for interpretation of construction of datatype

tuned

separated Random.thy from Quickcheck.thy

yet another useful lemma

dropped dangerous antiquotation

tuned

continued

tuned

better improvement in instantiation target

*** empty log message ***

raw_loop: more graceful crash recovery;

added exception CONTEXT, indicating context of another exception; exn_message: explicit context, *not* ML_Context.get_context; toplevel_error/apply: explicit exn_context; explicit Markup.location for exn_info (cf. at_command); fixed spelling; tuned;

added location;

schedule main control: more robust interrupting of potentially running threads;

message: proper root element for XML output; token_translation: proper Output.output of content;

Proof.put_thms false;

put_facts: do_props, i.e. facts are indexed by proposition again;

put_thms: pass do_props;

tuned

dropped "include" feature of classes

some theorems named explicitly

exported suffix

fixed typo

adjusted to current implementation

instance fun :: (finite, countable) countable

tuned

added Option_ord.thy

dropped local tsigs

some steps towards a refined treatment of equality

generic improvable syntax for targets

added hithero missing overloading.ML

tuned

whitespace tuning

clarified proposition

tuned proofs

canonical order on option type

added entries

check ISABELLE_BROWSER_INFO before cd;

replaced execute by system_out;

replaced execute by system_out;

added dummy version of string_of_pid;

use "ML-Systems/universal.ML"; specific system_out;

replaced execute by system_out;

proper dependency on ML-Systems/mosml.ML;

specific system_out (MosML lacks structure Posix); dummy implementation of Posix.ProcEnv.getpid;

* system/system_out provides a robust way to invoke external shell commands, with propagation of interrupts (after Poly/ML 5.2);

system_out: threaded version does not work for 5.1;

common setup for system_out/system;

added ML-Systems/system_shell.ML;

removed obsolete THIS_IS_ISABELLE_BUILD;

obsolete (cf. ML-Systems/polyml_common.ML);