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;

ML_Antiquote.value;

added isaantiqopen/close;

Logic.all/mk_equals/mk_implies; Term.all;

moved implies to logic.ML; removed equals; qualified all;

added all, is_all; improved dest_all; added implies (from term.ML);

Logic.implies;

Logic.is_all;

Term.all;

Logic.all/mk_equals/mk_implies;

session name: empty for Pure and by default;

induct_tac: allow omission of arguments;

info: default name is "", not "Pure";

moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;

removed obsolete dest_concls;

induct_tac: mutual rules work as for method "induct";

tuned get_inductT: *all* rules for missing instantiation; exported get_inductT;

induct_tac: infer mutual rule from types, as for proper induct method;

induct_tac/case_tac: nested tuples are split as expected;

induct_tac: old conjunctive rules no longer supported;

updated generated file;

induct_tac: rule is inferred from types;

cleaned up some proofs; removed unused stuff about totally-ordered sets; import Main

use new-style abbreviation/notation for fix syntax

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

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;