| Sat, 04 Mar 2000 11:52:42 +0100 |
paulson |
tidied
|
changeset |
files
|
| Sat, 04 Mar 2000 11:42:12 +0100 |
paulson |
new theories UNITY/Detects, UNITY/Reachability
|
changeset |
files
|
| Fri, 03 Mar 2000 21:02:45 +0100 |
wenzelm |
added con_elim_s(olved_)tac;
|
changeset |
files
|
| Fri, 03 Mar 2000 21:01:57 +0100 |
wenzelm |
mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac;
|
changeset |
files
|
| Fri, 03 Mar 2000 21:00:58 +0100 |
wenzelm |
added multi_resolveq, resolveq_tac;
|
changeset |
files
|
| Fri, 03 Mar 2000 18:26:19 +0100 |
paulson |
Added Tanja's Detects and Reachability theories. Also
|
changeset |
files
|
| Fri, 03 Mar 2000 18:22:53 +0100 |
paulson |
improved reasoning about {} and UNIV
|
changeset |
files
|
| Fri, 03 Mar 2000 02:00:43 +0100 |
wenzelm |
join_rules: compatibility check;
|
changeset |
files
|
| Fri, 03 Mar 2000 01:58:57 +0100 |
wenzelm |
token_trans: symbol length;
|
changeset |
files
|
| Thu, 02 Mar 2000 18:18:59 +0100 |
wenzelm |
join induct rules;
|
changeset |
files
|
| Thu, 02 Mar 2000 18:18:31 +0100 |
wenzelm |
added 'prolog' method;
|
changeset |
files
|
| Thu, 02 Mar 2000 18:18:10 +0100 |
wenzelm |
added freeze_all;
|
changeset |
files
|
| Thu, 02 Mar 2000 10:29:29 +0100 |
paulson |
polished version of the Allocator using Rename
|
changeset |
files
|
| Thu, 02 Mar 2000 10:26:22 +0100 |
paulson |
tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and
|
changeset |
files
|