tuned;

added datatype category;

replaced datatype kind by OuterKeyword.category;

clean: HOL-Plain;

prove lemma finite in context of finite class

added HOL-Plain;

explicit identification of toplevel commands, with status etc.; explicit point for tty mode; prompt: markup prev id; tuned signature;

added name_of; added get_id/put_id; tuned;

added get_id/put_id;

(removed Complex/ROOT.ML)

HOL += HOL-Complex

HOL += HOL-Complex

tuned

HOL += HOL-Complex

put file dependencies on separate lines

range_composition no longer in simp set

remove simp attribute from range_composition

rename INF to INFM

remove unused lemmas ub2ub_monofun' and dir2dir_monofun

remove redundant instance proof finite_po < cpo

remove unused lemma is_lub_Iup'

replace lub (range Y) with (LUB i. Y i)

add file dependencies

universal bifinite domain

isomorphisms between naturals and sums, products, and finite sets

theory of algebraic deflations

theory of eventually-constant sequences

rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM

rename compact_approx to compact_take

rename approx_pd to pd_take

split Completion.thy from CompactBasis.thy

filemap for CVS -> Mercurial conversion;

reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma

New theory of deflations and embedding-projection pairs

remove unused Cset.thy

added facts to lemma swap_simps and tuned lemma calc_atms

simplified retrieval of theory names of consts and types

tagged arities

HOL-Complex with proof terms

code generator setup for "int" also works under eta-contraction

added ML/ml_thms.ML;

tuned;

tuned;

additional ML antiquotations;

moved theorem values to ml_thms.ML;

Isar theorem values within ML.

added ML/ml_thms.ML;

updated generated file;

allow overlap of minor keywords and commands;

include HOL-Plain;

tuned args parser (cf. args.ML); tuned signature;

replaced simple_text by fully-featured parse_args;

tuned nested args parser; export generic_args1;

@{lemma}: 'by' keyword;

ML: improved antiquotations;

added macro interface; added @{let}, @{note};

tuned;

added thm_name, opt_thm_name;

adjusted import

adjusted import

added a lemma to at_swap_simps

remove cset theory; define ideal completions using typedef instead of cpodef

Args.theory;

added context/theory scanner;

Args.context;

fix: need to beta/eta normalize

established Plain theory and image

added dummy citiation

dropped recdef

class theory name lookup improved

modernized specifications;

tuned proofs;

modernized specifications;

modernized specifications;

typo

re-use official outer keywords;

scan: prefer command over keyword, allowing lexicons to overlap;

moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces; lexicons: allow overlapping keywords/commands -- warning instead of error;

moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces; moved check_text here;

antiquote: need to quote outer keywords;

tuned;

moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;

- Equivariance simpset used in proofs of strong induction and inversion rules now contains perm_simproc_app and perm_simproc_fun as well - first_order_matchs now eta-contracts terms before matching - Rewrote code for proving strong inversion rule to avoid failure when one of the arguments of the inductive predicate has an atom type

pprint: back to proper output of markup, with workaround for Poly/ML crash;

back to 1.36 (Poly/ML crash!?);

updated generated file;

YXML: no special treatment of white space;

pprint: proper output of markup (important for token translation);

ml_code_antiq: proper scanner combinators; ML_Antiquote.value;

moved concrete antiquotations to ml_antiquote.ML;

Antiquote.Open/Close;

add_antiq: more general notion of ML antiquotation; eval_antiquotes: support blocks and background context; moved concrete antiquotations to ml_antiquote.ML;

added Open/Close -- checked blocks;

added pprint_thy_ref;

Common ML antiquotations.

added ML/ml_antiquote.ML;