Fri, 13 Nov 2009 14:14:04 +0100 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
changeset |
files
|
Fri, 13 Nov 2009 14:03:24 +0100 |
krauss |
a few lemmas for point-free reasoning about transitive closure
|
changeset |
files
|
Fri, 13 Nov 2009 11:34:05 +0000 |
paulson |
merged
|
changeset |
files
|
Fri, 13 Nov 2009 11:33:33 +0000 |
paulson |
A number of theorems contributed by Jeremy Avigad
|
changeset |
files
|
Fri, 13 Nov 2009 06:24:31 +0100 |
bulwahn |
merged
|
changeset |
files
|
Thu, 12 Nov 2009 21:14:42 +0100 |
bulwahn |
merged
|
changeset |
files
|
Thu, 12 Nov 2009 20:39:02 +0100 |
bulwahn |
adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
|
changeset |
files
|
Thu, 12 Nov 2009 20:38:59 +0100 |
bulwahn |
removed annoying tracing message
|
changeset |
files
|
Thu, 12 Nov 2009 20:38:57 +0100 |
bulwahn |
added a tabled implementation of the reflexive transitive closure
|
changeset |
files
|
Thu, 12 Nov 2009 14:32:21 -0800 |
huffman |
merged
|
changeset |
files
|
Thu, 12 Nov 2009 14:31:29 -0800 |
huffman |
merged
|
changeset |
files
|
Thu, 12 Nov 2009 14:31:11 -0800 |
huffman |
improved ML interface to pcpodef
|
changeset |
files
|
Wed, 11 Nov 2009 10:15:32 -0800 |
huffman |
use Drule.standard (following typedef package), add pcpodef tactic interface
|
changeset |
files
|
Thu, 12 Nov 2009 22:29:54 +0100 |
wenzelm |
eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
|
changeset |
files
|
Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
changeset |
files
|