moved theorem kinds from PureThy to Thm;

LocalTheory.notes/defs: proper kind;

LocalTheory.axioms/notes/defs: proper kind; simplified Proof.theorem(_i);

simplified Proof.theorem(_i);

LocalTheory.axioms/notes/defs: proper kind; context_notes: ProofContext.set_stmt after import;

Optimized class_pairs for the common case of no subclasses

Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists

New transformation of eliminatino rules: we simply replace the final conclusion variable by False

run poly-4.9.1 as stable and poly-4.2.0 as experimental on at

removed legacy ML setup;

converted legacy ML scripts;

converted legacy ML scripts;

HOL-Prolog: converted legacy ML scripts;

start at-sml earlier and on different machine, remove sun-sml test (takes too long)

HOL-Algebra: converted legacy ML scripts;

profiling disabled

code thms for classops violating type discipline ignored

cleanup

added instance for class size

added combinators and lemmas

using class instance

dvd_def now with object equality

op div/op mod now named without leading op

workaround for definition violating type discipline

moved dvd stuff to theory Divides

re-eliminated thm trichotomy

power is now a class

tuned

clarified module dependencies

div is now a class

reduced verbosity

adjustments for class package

added an intro lemma for freshness of products; set up the simplifier so that it can deal with the compact and long notation for freshness constraints (FIXME: it should also be able to deal with the special case of freshness of atoms)

more robust syntax for definition/abbreviation/notation;

'notation': more robust 'and' list;

updated;

added Isar.goal;

added where_;

add lemmas LIM_zero_iff, LIM_norm_zero_iff

Includes type:sort constraints in its code to collect predicates in axiom clauses.

Now includes only types used to instantiate overloaded constants in arity clauses

added General/basics.ML;

moved some fundamental concepts to General/basics.ML;

Fundamental concepts.

add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);

tuned proofs;

replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected;

replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected; declared intro/elim rules;

dropping accidental self-imports

corrected polymorphism check

clarified code for building function equation system; explicit check of type discipline

moved evaluation to Code_Generator.thy

added filter_set; adaptions to more strict type discipline for code lemmas

moved transitivity rules to Orderings.thy

added transitivity rules, reworking of min/max lemmas

dropped dependency on sets

reworking of min/max lemmas

added interpretation

removed HOL_css

added evaluation oracle

replaced exists_fresh lemma with a version formulated with obtains; old lemma is available as exists_fresh' (still needed in apply-scripts)

updated;

Auxiliary antiquotations for Isabelle manuals.

common antiquote_setup.ML;

Arity clauses are now produced only for types and type classes actually used.

converted to 'inductive2';

added for_simple_fixes, specification;

replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);

removed fix_frees interface; added auto_fixes (depends on body mode);

converted to 'inductive2'; proper localized definitions; added rec examples;

inductive: canonical specification syntax (flattened result only); inductive_cases: local_theory; mk_cases/ind_cases: removed legacy code, proper treatment of fixed variables; get_inductive etc.: Proof.context; removed old trace/debug code; tuned;

inductive2: canonical specification syntax; ind_cases2: proper treatment of fixed variables;

InductivePackage.add_inductive_i: canonical argument order;

inductive2: canonical specification syntax;

Exported some names

simplified Proof.theorem(_i) interface -- removed target support; removed obsolete global_goal interface; removed goal_names, simplified goal kind output; tuned;

simplified Proof.theorem(_i) interface; simplified goal kind output;

antiquotation theory: plain Theory.requires, no peeking at ThyInfo;

simplified Proof.theorem(_i) interface;

tuned antiquotation theory;

value restriction

removed old cygwin wrappers;

declare_constraints: reset constraint on dummyS;

removed Isar/isar_thy.ML;

added dummyS;

removed legacy read/cert/string_of; removed obsolete IsarThy.theorem_i; tuned comments;

recdef_tc(_i): local_theory interface via Specification.theorem_i; incorporated IsarThy into IsarCmd;

incorporated IsarThy into IsarCmd;

removed theorem(_i); incorporated into IsarCmd;

upd

atbroy51 broke down, switch to atbroy9

updated

antiquotation "theory": proper output, only check via ThyInfo.theory;

tuned;

added antiquotation @{theory name};

fixed comment -- oops;

adjusted to new fun''

*** empty log message ***

added antiquotation theory

cleaned up

added theory antiquotation

combinator for overwriting changes with warning

added higher-order combinators for structured results

adjusted name in generated code

dropped LOrder dependency

moved upwars in HOL theory graph

added thy dependencies

PreList = Main - List

introduces preorders

dropped Inductive dependency

dropped Typedef dependency

added LOrder dependency

tuned ml antiquotations

adjusted

tuned

added tt tag

auto_term => lexicographic_order

updated

replaced "auto_term" by the simpler method "relation", which does not try to simplify. Some more cleanup.

added fresh_prodD, which is included fresh_prodD into mksimps setup;