Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-50
-32
+32
+50
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-50
-32
+32
+50
+100
+300
+1000
+3000
+10000
+30000
tip