summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

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);