| Wed, 02 Aug 2000 16:07:32 +0200 | paulson | coercion "intify" to remove type constraints from integer algebraic laws | changeset | files |
| Wed, 02 Aug 2000 16:06:54 +0200 | paulson | tidying and speeding up proofs | changeset | files |
| Wed, 02 Aug 2000 13:17:11 +0200 | nipkow | *** empty log message *** | changeset | files |
| Wed, 02 Aug 2000 11:30:38 +0200 | nipkow | *** empty log message *** | changeset | files |
| Tue, 01 Aug 2000 18:26:34 +0200 | paulson | used natify with div and mod; also put in the divide-by-zero trick | changeset | files |
| Tue, 01 Aug 2000 15:28:21 +0200 | paulson | natify, a coercion to reduce the number of type constraints in arithmetic | changeset | files |
| Tue, 01 Aug 2000 13:43:22 +0200 | wenzelm | tuned msg; | changeset | files |
| Tue, 01 Aug 2000 13:41:23 +0200 | wenzelm | * blast(_tac) now handles actual object-logic rules as assumptions; | changeset | files |
| Tue, 01 Aug 2000 11:58:27 +0200 | wenzelm | added all_eq, imp_eq (for blast); | changeset | files |
| Tue, 01 Aug 2000 11:58:14 +0200 | wenzelm | improved comments; | changeset | files |
| Tue, 01 Aug 2000 11:57:09 +0200 | wenzelm | handle actual object-logic rules by atomizing the goal; | changeset | files |
| Tue, 01 Aug 2000 11:55:27 +0200 | wenzelm | added atomize_goal / atomize_tac; | changeset | files |
| Tue, 01 Aug 2000 00:20:12 +0200 | wenzelm | (un)fold: CHANGED; | changeset | files |
| Tue, 01 Aug 2000 00:19:07 +0200 | wenzelm | added has_meta_prems; | changeset | files |
| Tue, 01 Aug 2000 00:18:40 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 31 Jul 2000 14:37:18 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 31 Jul 2000 14:33:40 +0200 | wenzelm | updated 'obtain'; | changeset | files |
| Mon, 31 Jul 2000 12:50:33 +0200 | nipkow | Removed Quot | changeset | files |
| Mon, 31 Jul 2000 12:33:26 +0200 | nipkow | Never used and not relevant. | changeset | files |
| Sun, 30 Jul 2000 13:06:20 +0200 | wenzelm | obtain; | changeset | files |
| Sun, 30 Jul 2000 13:04:58 +0200 | wenzelm | added split_bind_asm, bind_splits; | changeset | files |
| Sun, 30 Jul 2000 13:03:49 +0200 | wenzelm | adapted obtain; | changeset | files |
| Sun, 30 Jul 2000 13:02:56 +0200 | wenzelm | removed equalityCE; | changeset | files |
| Sun, 30 Jul 2000 13:02:14 +0200 | wenzelm | added atomic_Trueprop; | changeset | files |
| Sun, 30 Jul 2000 13:01:50 +0200 | wenzelm | updated ObtainFun; | changeset | files |
| Sun, 30 Jul 2000 13:01:09 +0200 | wenzelm | 'def': no constraint on variable; | changeset | files |
| Sun, 30 Jul 2000 12:56:14 +0200 | wenzelm | exporter setup for context elements; | changeset | files |
| Sun, 30 Jul 2000 12:55:36 +0200 | wenzelm | export RANGE, hard_asm_tac, soft_asm_tac; | changeset | files |
| Sun, 30 Jul 2000 12:54:07 +0200 | wenzelm | turned into plain context element; | changeset | files |
| Sun, 30 Jul 2000 12:53:22 +0200 | wenzelm | local_def(_i): no constraint on var; | changeset | files |