added lemma exE_some (from specification_package.ML);

Simplifier.theory_context;

tuned error msg; tuned;

Simplifier.context/theory_context;

updated;

new interface to make_conjecture_clauses

* Simplifier: simpset of a running simplification process contains a proof context; * Simplifier.inherit_context supercedes Simplifier.inherit_bounds; * Simplifier/Classical Reasoner: more abstract interfaces change_simpset/claset;

added type_solver (uses Simplifier.the_context); removed obsolete context_type_solver;

added pos/negDivAlg_induct declarations (from Main.thy);

moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy; change_simpset;

removed obsolete/experimental context components (superceded by Simplifier.the_context); more abstract change_simpset(_of); tuned;

added set/addloop' for simpset dependent loopers; simpset: added context field with the_context, set_context; added inherit_context (inherits bounds as well); removed obsolete inherit_bounds;

functor: no Simplifier argument; change_simpset;

change_claset(_of): more abtract interface; claset_of: init proof context; added raw get_claset;

functor: no Simplifier argument; export change_clasimpset;

tuned;

Simplifier.inherit_context instead of Simplifier.inherit_bounds;

change_claset/simpset;

change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;

Improved proof of injectivity theorems to make it work on "ordinary" function types as well.

Fixed bug in proof of support theorem (it failed on constructors with no arguments).

Implemented proofs for support and freshness theorems.

deleted leading space in the definition of fresh

Initial revision.

tuned;

tuned comment;

added ML_type, ML_struct;

more;

* antiquotations ML_type, ML_struct; * Isar 'guess' element;

added guess;

added antiquotations ML_type, ML_struct;

use perl for test/stat;

export strip_params;

note_thmss, read/cert_vars etc.: natural argument order; added string_of_thm; tuned;

goal statements: before_qed argument;

added 'guess', which derives the obtained context from the course of reasoning;

added primitive_text, succeed_text;

goal statements: accomodate before_qed argument; ProofContext.note_thmss_i: natural argument order;

goal statements: accomodate before_qed argument;

added 'guess';

tuned;

added no_facts;

tuned comments;

updated;

signature changes

added module rat.ML for rational numbers

longer time out for test (kleing)

deletion of Tools/res_types_sorts; removal of absolute numbering of clauses

deletion of Tools/res_types_sorts; removal of absolute numbering of clauses

obsolete;

counter added to SAT signature

no proof reconstruction when quick_and_dirty is set

tidying

domain package generates compactness lemmas for new constructors

add ML bindings for compactness lemmas

added compactness theorems

added compactness lemmas; cleaned up

added compactness theorems in locale iso

added several theorems in locale iso

added xsymbols syntax for pairs; cleaned up

added theorem typedef_compact

rearranged subsections; added theorems expand_cfun_eq, expand_cfun_less

cleaned up; renamed less_fun to expand_fun_less

added hd lemma

simplifying the treatment of clausification

simplifying the treatment of nameless theorems

expand: error on undefined/empty env variable; tuned;

added assert; tuned;

tuned;

added string_of_pid;

raw symbols: allow non-ASCII chars (e.g. UTF-8); tuned comment;

moved string_of_pid to ML-Systems;

ML_SUFFIX in targets (experimental);

cleanup backup images;

small tidy-up of utility functions

updated print_tac;

add names to infix declarations

new syntax translations for continuous lambda abstraction

removed Istrictify; simplified some proofs

added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up

cleaned up

added theorem typedef_chfin

replaced foldr' with foldr1

cleaned up; renamed "Porder.op <<" to "Porder.<<"

Tactics sat and satx reimplemented, several improvements

tuned Memory.hilim;

get rid of feeder -- at the cost of batch-only commit-at-exit; redirect stderr to stdout;

*** empty log message ***

-nort option;

added could_unify;

more efficient check_specified, much less invocations; Type.could_unify filter;

moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;

uses susp.ML, lazy_seq.ML, lazy_scan.ML;

added Import/susp.ML, Import/lazy_seq.ML, Import/lasy_scan.ML;

minor tweaks for Poplog/PML; removed chars;

tuned memory limits; Int/IntInf: more compat stuff; proper use/use_string -- cf. run-poplogml;

Int.max;

minor tweaks for Poplog/PML; removed redundant max function;

minor tweaks for Poplog/PML;

initial pop11 code for ML use/use_string; ML_SUFFIX;

Poplog/PML: ML_SUFFIX=.psv;

support ML_SUFFIX;

obsolete;

fix due to new neq_simproc

removed obsolete comment;

added idtypdummy_ast_tr; removed obsolete k_tr;

added syntax for _idtdummy, _idtypdummy; removed obsolete _K;

added absdummy;

removed obsolete dummy_pat_tr;

Term.absdummy;

removed obsolete ex/Tuple.thy;

replaced _K by dummy abstraction;

print_translation: does not handle _idtdummy;

tuned;

added dummy variable binding; removed obsolete _K;

changes due to new neq_simproc in simpdata.ML

added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);

Term.str_of_term;

minor code tidyig

code restructuring