tuned;

monomorphic equality: let ML work out the details;

added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);

tuned Tactic signature;

removed obsolete Library.seq;

moved flip to library.ML; removed unused dest/unfold/unfold_rev; simplified fold/fold_rev/fold_map;

added CSUBGOAL;

cleaned up signature;

added downto0 (from library.ML);

merge_ss: plain merge of prems;

added flip (from General/basics.ML); renamed gen_submultiset to submultiset; moved downto0 to pattern.ML; moved legacy gen_merge_lists/merge_lists/merge_alists to Isar/locale.ML; moved plural to HOL/Tools/fundef_lib.ML; removed obsolete seq; simplified chop, fold2;

tuned document;

use antiquotations instead of raw TeX code; tuned document;

name_of_fqgar: precise type;

added plural (from Pure/library.ML); removed unused eq_str;

local open FundefLib;

renamed gen_submultiset to submultiset;

HOL-ex: tuned deps;

tuned list comprehension, added lemma

fixed tex error

*** empty log message ***

*** empty log message ***

extended

cosmetic

made SML/NJ happy;

added target/local_abbrev (from proof_context.ML); target_abbrev: demand equal head const (tool compliance);

moved specific target/local_abbrev to theory_target.ML;

"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases. more cleanup.

added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction

proper handling of Tools;

cosmetic

refute_tac made more deterministic

extended

cosmetic

tracing disabled

additional tracing information

tuned

some tests for arith added

Moved list comprehension into List

MiniSAT mentioned in comment

fixed handling of meta-logic propositions

simplified interfaces, some restructuring

updated

added some bibtex entries

Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)

Added simp-rules: "R O {} = {}" and "{} O R = {}"

rudimenary

tuned

dropped superfluous name bindings

localized

fixed typo

insert: canonical argument order;

simplified/unified list fold;

replace (- 1) with -1

simplify some proofs

tuned headers -- adapted to usual conventions;

moved Compute_Oracle from Pure/Tools to Tools;

proper theory setup for compute oracle (based on CPure); simplified oracle setup;

moved IsaPlanner from Provers to Tools; moved Compute_Oracle from Pure/Tools to Tools;

moved IsaPlanner from Provers to Tools;

made aconvc pervasive;

moved aconvc to more_thm.ML;

tuned ML setup;

decode_term: force qualified name into Const;

proper loading of ML files (in HOL.thy); moved Integ files to canonical place; misc cleanup;

HOL_proofs;

moved Integ files to canonical place;

proper loading of ML files;

removed dead code;

tuned header;

doc: exclude isabelle_isar.pdf;

tuned the proof

introduced symmetric variants of the lemmas for alpha-equivalence

proper loading of ML files; removed obsolete IFOL.thy/FOL.thy values;

removed obsolete IFOL.thy/FOL.thy values;

proper loading of ML files;

tuned header;

tuned oracle setup;

moved HOLCF tools to canonical place;

moved TFL files to canonical place;

moved TFL files to canonical place;

added src/Tools; moved TFL files to canonical place;

fixed title;

Tools: generic tools outside of Pure.

moved Integ files to canonical place;

fixed use_thy "LocalWeakening";

included new example in the compiling process

a theory using locally nameless terms and strong induction principles

tuned the proof

emulate later version of TextIO.inputLine;

reversed SML B library patches;

TextIO.inputLine: use present SML B library version;

tuned USEDIR_OPTIONS; PDF_VIEWER: try to be smart for MacOS (Darwin);

removed HOL4 image, which seldom works;

simplified data setup

instance: always print sorts on failure

more example

fixed typo

updated

generalized lemmas

eliminated strings

tuned

clarified error message

simplify names of locale interpretations

renamed some lemmas in Complex.thy

cleaned up proofs; reorganized sections; removed redundant lemmas

use new-style instance declarations

instance complex :: banach

add lemma real_sqrt_sum_squares_less

cleaned up some proofs

interpretation bounded_linear_divide

add bounded_linear lemmas

add isUCont lemmas

updated examples to include an instance of (lexicographic_order simp:...)

Complex: generalized type of exp

generalized exp to work over any complete field; new proof of exp_add

add type annotations for exp

interpretations additive_scaleR_left, additive_scaleR_right

remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs

new proof of Cauchy product formula for series