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

adapted to new nominal_inductive

Improved code generator for characters: now handles non-printable characters as well.

tuned proofs (taking full advantage of nominal_inductive)

adapted to nominal_inductive infrastructure

made the type sets instance of the "cp" type-class

added extended the lemma for equivariance of freshness

adapted to nominal_inductive

adapted to new nominal_inductive infrastructure

Adapted to new syntax of nominal_inductive.

Adapted to changes in nominal_inductive.

Implemented proof of strong induction rule.

Exported perm_of_pair, mk_not_sym, and perm_simproc.

cleaned up HOL/ex/Code*.thy

fixed document preparation

fixed problem with mutual recursion

cleaned up Library/ and ex/

minimal intro rules

exported interface for intro rules