| Thu, 08 Jan 1998 18:09:07 +0100 |
oheimb |
added select_equality to the implicit claset
|
changeset |
files
|
| Thu, 08 Jan 1998 18:08:43 +0100 |
oheimb |
added select_equality to the implicit claset
|
changeset |
files
|
| Thu, 08 Jan 1998 18:07:06 +0100 |
oheimb |
added newline at end of file
|
changeset |
files
|
| Thu, 08 Jan 1998 18:06:21 +0100 |
oheimb |
*** empty log message ***
|
changeset |
files
|
| Thu, 08 Jan 1998 18:03:36 +0100 |
oheimb |
streamlined specification of included theories
|
changeset |
files
|
| Thu, 08 Jan 1998 18:00:42 +0100 |
oheimb |
corrected Title
|
changeset |
files
|
| Thu, 08 Jan 1998 18:00:08 +0100 |
oheimb |
removed obsolete comment
|
changeset |
files
|
| Thu, 08 Jan 1998 17:56:32 +0100 |
oheimb |
added Univalent
|
changeset |
files
|
| Thu, 08 Jan 1998 17:47:22 +0100 |
oheimb |
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
|
changeset |
files
|
| Thu, 08 Jan 1998 17:44:50 +0100 |
oheimb |
added update_same, update_other, update_triv, and map_of_SomeD
|
changeset |
files
|
| Thu, 08 Jan 1998 17:42:26 +0100 |
oheimb |
replaced fn _ => by K
|
changeset |
files
|
| Thu, 08 Jan 1998 16:52:31 +0100 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Thu, 08 Jan 1998 11:24:46 +0100 |
paulson |
New rule: image_subset
|
changeset |
files
|
| Thu, 08 Jan 1998 11:23:18 +0100 |
paulson |
Restored the ciphertext in OR4 in order to make the spec closer to that in
|
changeset |
files
|
| Thu, 08 Jan 1998 11:21:45 +0100 |
paulson |
Tidied by adding more default simprules
|
changeset |
files
|
| Wed, 07 Jan 1998 13:55:54 +0100 |
wenzelm |
adapted to new split order;
|
changeset |
files
|
| Wed, 07 Jan 1998 13:55:29 +0100 |
wenzelm |
adapted to new sort function;
|
changeset |
files
|
| Wed, 07 Jan 1998 13:53:42 +0100 |
wenzelm |
improved targets;
|
changeset |
files
|
| Tue, 06 Jan 1998 12:32:43 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 05 Jan 1998 12:56:22 +0100 |
wenzelm |
added -u option (again);
|
changeset |
files
|
| Mon, 05 Jan 1998 10:47:10 +0100 |
paulson |
Now calls Blast_tac more often
|
changeset |
files
|
| Fri, 02 Jan 1998 18:47:31 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 02 Jan 1998 18:40:30 +0100 |
wenzelm |
feeder;
|
changeset |
files
|
| Fri, 02 Jan 1998 17:17:24 +0100 |
paulson |
Changed required by new blast_tac (the one that squashes flex-flex pairs)
|
changeset |
files
|
| Fri, 02 Jan 1998 17:16:39 +0100 |
paulson |
Blast_tac now squashes flex-flex pairs immediately
|
changeset |
files
|
| Fri, 02 Jan 1998 17:15:52 +0100 |
paulson |
New theorem image_subsetI
|
changeset |
files
|
| Fri, 02 Jan 1998 17:15:19 +0100 |
paulson |
Making proofs faster, especially using keysFor_parts_insert
|
changeset |
files
|
| Fri, 02 Jan 1998 13:24:53 +0100 |
wenzelm |
do require perl;
|
changeset |
files
|
| Fri, 02 Jan 1998 11:59:06 +0100 |
paulson |
Auto_tac now has type tactic, not unit->tactic
|
changeset |
files
|
| Fri, 02 Jan 1998 11:17:06 +0100 |
paulson |
Declared startTiming and endTiming
|
changeset |
files
|