import_export_proof: simplified thm definition -- PureThy.name_thm does the job;

added query_type/const/class (meta data);

the_tags: explicit error message; new_decl: Position.thread_data;

activate_context: strict the_context, no fallback on theory context;

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