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 -56 +56 +100 +300 +1000 +3000 +10000 +30000 tip

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
tuned the proof of transitivity/narrowing
2005-12-15, by urbanc
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
2005-12-15, by paulson
made further tunings
2005-12-15, by urbanc
Added functions to test equivalence between clauses.
2005-12-15, by mengj
ex/Sudoku.thy
2005-12-14, by webertj
deleted redundant (looping!) simprule
2005-12-14, by paulson
modified example for new clauses
2005-12-14, by paulson
removal of some redundancies (e.g. one-point-rules) in clause production
2005-12-14, by paulson
removed unused function repeat_RS
2005-12-14, by paulson
Changed literals' ordering and the functions for sorting literals.
2005-12-14, by mengj
1. changed fol_type, it's not a string type anymore.
2005-12-14, by mengj
changed ATP input files' names and location.
2005-12-14, by mengj
Potentially infinite lists as greatest fixed-point.
2005-12-13, by wenzelm
Provers/induct: coinduct;
2005-12-13, by wenzelm
tuned proofs;
2005-12-13, by wenzelm
added HOL/Library/Coinductive_List.thy;
2005-12-13, by wenzelm
added a fresh_left lemma that contains all instantiation
2005-12-13, by urbanc
initial commit (not to be seen by the public)
2005-12-13, by urbanc
simpset for computation in raw_arith_tac added just as comment, nothing changed!
2005-12-13, by chaieb
deals with Suc in mod expressions
2005-12-13, by chaieb
Poplog/pml provides a proper print function already!
2005-12-13, by wenzelm
meson no longer does these examples
2005-12-13, by paulson
now generates the name "append"
2005-12-13, by paulson
removal of functional reflexivity axioms
2005-12-13, by paulson
list_of_indset now also generates code for set type.
2005-12-13, by berghofe
added generic name mangler
2005-12-12, by haftmann
improvement in eq handling
2005-12-12, by haftmann
improvements in class and eq handling
2005-12-12, by haftmann
added dummy 'print' to non-polyml systems
2005-12-12, by haftmann
ISAR-fied some proofs
2005-12-11, by urbanc
completed the sn proof and changed the manual
2005-12-11, by urbanc
changed the types in accordance with Florian's changes
2005-12-10, by urbanc
substantial improvements for class code generation
2005-12-09, by haftmann
improved extraction interface
2005-12-09, by haftmann
tuned
2005-12-09, by urbanc
oriented result pairs in PureThy
2005-12-09, by haftmann
tuned;
2005-12-08, by wenzelm
removed Syntax.deskolem;
2005-12-08, by wenzelm
swap: no longer pervasive;
2005-12-08, by wenzelm
replaced swap by contrapos_np;
2005-12-08, by wenzelm
tuned proofs;
2005-12-08, by wenzelm

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

isabelle