Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
adapted example
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
removed obsolete, harmful step in tactic
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
removed (co)iterators from documentation
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
avoid duplicate 'disc_iff' theorems
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
life without 'metis'
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalize internals
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
compile
|
changeset |
files
|
Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
make 'diff_iff' a simp rule if available
|
changeset |
files
|