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;

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!

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