added read_def_cterms, read_cterm (from thm.ML);

cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; Term.string_of_vname;

cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; avoid rep_theory;

removed Pure/Syntax/ROOT.ML;

Term.string_of_vname;

Theory.inferT_axm;

do not enable Toplevel.debug globally;

cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;

canonical merge operations

declarations: apply target_morphism;

inst(T)_morphism: avoid reference to static theory value;

tuned signature; export: precomputed closure, no reference to contexts;

added Morphism.transform/form (generic non-sense);

Morphism.transform/form;

data declaration: removed obsolete target_morphism (still required for local data!?);

data declaration: removed obsolete target_morphism;

added eval_antiquotes_fn (tmp);

tuned document (headers, sections, spacing);

do translation: CONST;

eval_antiquotes: proper parentheses for projection;

canonical merge operations

Removed erroneous application of rev in get_clauses that caused introduction rules taken from the InductivePackage database to be in the wrong order.

more robust proof

Experimental code for the interpretation of definitions.

Experimental interpretation code for definitions.

New file for locale regression tests.

debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal

minimize imports

new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports

moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy

added proj_value_antiq;

absdummy: use internal name uu to avoid renaming of popular names;

tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts

updated;

output_basic: added isaantiq markup (only inside verbatim tokens);

newenvironment{isaantiq};

Zero variable indexes in clauses

Improved treatment of classrel/arity clauses

Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)

Improved and simplified the treatment of classrel/arity clauses

canonical merge operations

moved nonstandard limit stuff from Lim.thy into new theory HLim.thy

run annomaly from makedist

set special ISABELLE_USER_HOME as in other isatest settings

isatest version of annomaly script. to be run from istatest-makedist.

new standard proof of lemma LIM_inverse

new class syntax for scaleR and norm classes

removed debugging code

canonical merge operations

tuned

dropped legacy ML bindings

moved nonstandard stuff from SEQ.thy into new file HSEQ.thy

move lemma real_of_nat_inverse_le_iff from NSA.thy to NthRoot.thy

new standard proof of convergent = Cauchy

new standard proof of LIMSEQ_realpow_zero

new LIM/isCont lemmas for abs, of_real, and power

some restructuring

interpretation bounded_linear_of_real

removed unnecessary premise from power_le_imp_le_base

proper handling of morphisms

Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.

inline_antiq: no longer forces ML_Syntax.atomic;

removed dead code

tuned

added example for definitions in local contexts

removed obsolete workaround

generalized type of lemma setsum_product

new standard proofs of some LIMSEQ lemmas

rearranged sections

remove redundant lemmas

removed obsolete workarounds

deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)

tuned slightly the previous commit

perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a

add new standard proofs for limits of sequences

Replaced add_inductive_i by add_inductive_global.

- Tried to make name_of_thm more robust against changes of the structure of proofs. - Now uses add_inductive_global rather than add_inductive_i for the definition of the realizability predicate.

- Removed occurrences of ProofContext.export in add_ind_def that caused theorems to end up in the wrong context - Explicit parameters are now generalized in theorems returned by add_inductive(_i)

thy_deps: sort Context.thy_ord;

added thy_ord -- order of creation; ancestors: back to traditional ad-hoc order (avoid occasional problems with get_thm);

simplified thy_deps using Theory.ancestors_of (in order of creation);

renamed Variable.importT to importT_thms;

removed unused dep_graph;

theory: maintain ancestors in order of creation;

rep_thm/cterm/ctyp: removed obsolete sign field; renamed Variable.importT to importT_thms;

rebind HOL.refl as refl (hidden by widen.refl);

rep_thm/cterm/ctyp: removed obsolete sign field;

make fresh_guess fail if it does not solve the subgoal

add a few details in the Fst and Snd cases of unicity proof

find_first is just an alias

added print_mode (generic non-sense);

improved exception CTERM; removed obsolete sign_of/sign_of_thm;

removed unused info channel; renamed Output.has_mode to print_mode_active; cleaned-up Output functions;

added print_mode;

removed unused info channel;

renamed Output.has_mode to print_mode_active;