| Fri, 31 Aug 2012 15:04:03 +0200 |
blanchet |
optimized "mk_case_disc_tac"
|
changeset |
files
|
| Fri, 31 Aug 2012 15:04:03 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 31 Aug 2012 15:04:03 +0200 |
blanchet |
rationalized data structure for distinctness theorems
|
changeset |
files
|
| Fri, 31 Aug 2012 15:04:03 +0200 |
blanchet |
optimized "case_cong" proof
|
changeset |
files
|
| Fri, 31 Aug 2012 15:04:03 +0200 |
blanchet |
allow default names for selectors via wildcard (_) + fix wrong index (k)
|
changeset |
files
|
| Fri, 31 Aug 2012 15:04:03 +0200 |
blanchet |
minor fixes (for compatibility with existing datatype package)
|
changeset |
files
|
| Fri, 31 Aug 2012 15:04:03 +0200 |
blanchet |
generate "split_asm" property
|
changeset |
files
|
| Fri, 31 Aug 2012 15:04:03 +0200 |
blanchet |
generate "split" property
|
changeset |
files
|
| Fri, 31 Aug 2012 16:35:30 +0200 |
wenzelm |
more precise register_proofs for local goals;
|
changeset |
files
|
| Fri, 31 Aug 2012 15:25:26 +0200 |
wenzelm |
more informative error message from failed goal forks (violating old-style TTY protocol!);
|
changeset |
files
|
| Fri, 31 Aug 2012 15:24:26 +0200 |
wenzelm |
avoid empty tooltips;
|
changeset |
files
|
| Fri, 31 Aug 2012 15:03:44 +0200 |
wenzelm |
clarified command status (again);
|
changeset |
files
|