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;

updated use_text/file for 5.2;

moved use_text/file to polyml_old_compiler5.ML;

removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);

added ML-Systems/polyml-5.1.ML, ML-Systems/polyml_old_compiler4.ML, ML-Systems/polyml_old_compiler5.ML;

back to feeder -- Isabelle ML setup no longer evaluates command line;

simplified thm_antiq;

removed unused print_properties, print_position;

replaced obsolete /usr/proj by /home;

replaced obsolete /usr/proj by /home;

remote CVSROOT: default to atbroy100 instead of sunbroy2; adapted some paths;

tuned settings for target platforms;

thm_antiq: produce error at runtime, not compile time; tuned;

get_thms etc.: improved reporting of source position;

added pos_of_ref;

fixed proof;

Equivariance prover now uses permutation simprocs as well.

export add/del_thm;

added print_properties, print_position;

Facts.Named: include position;

tuned proofs

more antiquotations

Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned

added forward composition

Product_Type.apfst and Product_Type.apsnd

Theory Product_Type; fixed typos

rearranged

(continued)

tuned

tuned import

adjusted authorship

tuned proof

added theory Library/Enum.thy

tuned proofs

simplified get_thm(s): back to plain name argument; renamed former get_thm to get_fact_single, and get_thms to get_fact;

renamed former get_thms(_silent) to get_fact(_silent);

simplified get_thm(s): back to plain name argument; renamed former get_thms(_silent) to get_fact(_silent);

simplified get_thm(s): back to plain name argument;

more antiquotations;

avoid Auto_tac;

more antiquotations; eliminated change_claset/simpset;

eliminated change_claset/simpset;

auxiliary dynamic_thm(s) for fact lookup; renamed local dynamic_thm(s) to goal_thm(s);

auxiliary dynamic_thm(s) for fact lookup;

renamed datatype thmref to Facts.ref, tuned interfaces;

removed redundant Nat.less_not_sym, Nat.less_asym; renamed Nat.less_irrefl to less_irrefl_nat, no longer declared elim;

removed redundant Nat.less_irrefl;

Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts Sledgehammer no longer produces structured proofs by default.

system: writeln output, if available;

error tuning

moved typ_of_inst to Type.typ_of_sort

instantiation less liberal with dangling constraints

Type.lookup now curried

Type.lookup now curried; typ_of_sort

new class error case NoSubsort

quickcheck with term reconstruction

whitespace tuning

theory loader: discontinued *attached* ML scripts;

converted legacy ML scripts;

valid_thms: get_thms_silent;

removed check_lookup; added get_thms_silent;

added ckeck_lookup flag (default false), which controls sanity check of thm lookup;

updated generated files;

tuned proof;

removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);

removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy); renamed less_imp_le to less_imp_le_nat;

avoid rebinding of existing facts;

avoid rebinding of existing facts; removed duplicate lemmas;

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!