remove unused constant liftpair

simplify profinite class axioms

clean up and rename some profinite lemmas

move at-sml-dev-e to macbroy23

replace SetPcpo.thy with Cset.thy

updated for 2008; proper name of TUM;

(removed non-present change)

explicit thm context for error messages

using tages to find theory names

type constructors now with markup

fixed bind error for malformed primrec specifications

DatatypeProp.make_distincts: only one half of each symmetric pair is constructed

streamlined definitions

moved Float.thy to Library

removed SetPcpo.thy and cpo instance for type bool; added Cset.thy with pcpo type 'a cset isomorphic to 'a set; updated ideal completion theory to use cset

moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale

add lemma Abs_image

added some lemmas; reorganized into sections; tuned proofs

added some lemmas; tuned proofs

tuned

replace less_lift with flat_less_iff

tweak lemmas adm_all and adm_ball

move lemmas into locales; restructure some proofs

add lemmas take_chain_less and take_chain_le

disposed Sign.read_typ etc;

renamed is_abbrev_mode to abbrev_mode; added private get_sort (from sign.ML);

ProofContext.abbrev_mode;

moved get_sort to Isar/proof_context.ML; removed obsolete read_def_typ, read_typ, read_typ_syntax, read_typ_abbrev;

tuned signature; removed duplicates of read_typ/cert_typ (cf. RecordPackage.read_typ/cert_typ);

private add_used (from drule.ML); Variable.declare_names;

Variable.declare_typ;

added declare_typ;