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;

tuned comment;

cleaned-up Output functions; removed unused info channel; moved print_mode to ROOT.ML (generic non-sense);

improved exception CTERM; added instantiate_cterm; removed obsolete sign_of_thm;

added scanwords from library.ML (for obsolete rename_tac);

removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);

removed dead code;

cleaned-up Output functions;

eliminated obsolete rename_tac;

removed obsolete sign_of/sign_of_thm;

ML antiquotes;

tuned comments;

fixed chr/explode;

avoid overloaded integer constants (accomodate Alice);

avoid clash with Alice keywords;

signature: eqtype to accomodate Alice;

renamed comp to compose (avoid clash with Alice keywords);

renamed of_sort_derivation record fields (avoid clash with Alice keywords);

added ML-Systems/alice.ML;

renamed Variable.import to import_thms (avoid clash with Alice keywords);

removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);

ranamed CodegenData.lazy to lazy_thms (avoid clash with Alice keywords);

remove the lemma swap_fun which was not needed

slighltly improved the proof of unicity

Compatibility file for Alice 1.3 -- experimental!

rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name

optimizing the null instantiation case

now exports distinct_subgoal_tac (needed by MetisAPI)

exception handling

added reserved words mod, div for SML

added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas

Fixed bug in dest_prem: premises of the form "p x_1 ... x_n" (where p is a variable) are now treated as side conditions if p is not in the list of (global) parameters.

fixed typo

simplified constant representation in code generator

tuned

equality on strings

paraphrasing equality

updated

improved character output for SML

dropped legacy ML bindings

simplified some steps

MESON tactical takes an additional argument: the clausification function.

Now checks for types-only clause before outputting.

- Improved error messages in equivariance proof - Renamed <predicate>_eqvt to <predicate>.eqvt

Renamed induct(s)_weak to weak_induct(s) in order to unify naming scheme with the one used in nominal_inductive.

- Renamed <predicate>_eqvt to <predicate>.eqvt - Renamed induct_weak to weak_induct

the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive