isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

rule_context: numbered cases;
2005-12-22, by wenzelm
conjunction_tac: single goal;
2005-12-22, by wenzelm
renamed imp_cong' to imp_cong_rule;
2005-12-22, by wenzelm
mk_conjunction: proper treatment of bounds;
2005-12-22, by wenzelm
fixed has_internal;
2005-12-22, by wenzelm
Tactic.precise_conjunction_tac;
2005-12-22, by wenzelm
added locale meta_conjunction_syntax and various conjunction rules;
2005-12-22, by wenzelm
simplified setup: removed dest_concls, local_impI, conjI;
2005-12-22, by wenzelm
induct_rulify;
2005-12-22, by wenzelm
actually produce projected rules;
2005-12-22, by wenzelm
*.inducts holds all projected rules;
2005-12-22, by wenzelm
tuned;
2005-12-22, by wenzelm
tuned induct proofs;
2005-12-22, by wenzelm
mutual induct with *.inducts;
2005-12-22, by wenzelm
wf_induct_rule: consumes 1;
2005-12-22, by wenzelm
structure ProjectRule;
2005-12-22, by wenzelm
updated auxiliary facts for induct method;
2005-12-22, by wenzelm
slight improvements
2005-12-21, by haftmann
slight improvements in name handling
2005-12-21, by haftmann
slight refinements
2005-12-21, by haftmann
added eq_ord
2005-12-21, by haftmann
slight clean ups
2005-12-21, by haftmann
discontinued unflat in favour of burrow and burrow_split
2005-12-21, by haftmann
new hash table module in HOL/Too/s
2005-12-21, by paulson
modified suffix for [iff] attribute
2005-12-21, by paulson
removed or modified some instances of [iff]
2005-12-21, by paulson
tuned;
2005-12-20, by wenzelm
added .cvsignore
2005-12-20, by haftmann
removed improper .cvsignore
2005-12-20, by haftmann
removed superfluos is_prefix functions
2005-12-20, by haftmann
resolved shadowing of Library.find_first
2005-12-20, by haftmann
removed infix prefix, introduces burrow
2005-12-20, by haftmann
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
2005-12-20, by mengj
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
2005-12-20, by mengj
made the changes according to Florian's re-arranging of
2005-12-19, by urbanc
added proofs to show that every atom-kind combination
2005-12-19, by urbanc
added thms to perm_compose (so far only composition
2005-12-19, by urbanc
tuned one comment
2005-12-19, by urbanc
fixed a bug that occured when more than one atom-type
2005-12-19, by urbanc
fixed proof
2005-12-19, by nipkow
more cleaning up - this time of the cp-instance
2005-12-18, by urbanc
improved the finite-support proof
2005-12-18, by urbanc
improved the code for showing that a type is
2005-12-18, by urbanc
simp del: empty_Collect_eq;
2005-12-17, by wenzelm
sort_distinct;
2005-12-17, by wenzelm
added sort_distinct;
2005-12-17, by wenzelm
added container-lemma fresh_eqvt
2005-12-16, by urbanc
I think the earlier version was completely broken
2005-12-16, by urbanc
tuned more proofs
2005-12-16, by urbanc
new lemmas
2005-12-16, by nipkow
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
hashing to eliminate the output of duplicate clauses
2005-12-16, by paulson
hash tables from SML/NJ
2005-12-16, by paulson
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
there was a small error in the last commit - fixed now
2005-12-15, by urbanc
tuned more proof and added in-file documentation
2005-12-15, by urbanc
improved proofs;
2005-12-15, by wenzelm
acc_induct: proper tags;
2005-12-15, by wenzelm
removed obsolete/unused setup_induction;
2005-12-15, by wenzelm

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle