| Wed, 08 Mar 2000 16:17:10 +0100 | paulson | tidied | file | diff | annotate |
| Mon, 20 Sep 1999 10:46:16 +0200 | paulson | renamed Always_Int to Always_Int_I | file | diff | annotate |
| Wed, 01 Sep 1999 11:16:02 +0200 | paulson | tidied some proofs | file | diff | annotate |
| Mon, 16 Aug 1999 18:47:20 +0200 | paulson | deleted obsolete assignment | file | diff | annotate |
| Thu, 05 Aug 1999 22:11:43 +0200 | wenzelm | removed obsolete addsimps update_defs; | file | diff | annotate |
| Tue, 06 Jul 1999 21:13:12 +0200 | wenzelm | adapted to generic numerals; | file | diff | annotate |
| Fri, 21 May 1999 10:59:41 +0200 | paulson | updated comment | file | diff | annotate |
| Fri, 07 May 1999 11:02:00 +0200 | paulson | tidied | file | diff | annotate |
| Tue, 04 May 1999 10:26:00 +0200 | paulson | Invariant -> Always and other tidying | file | diff | annotate |
| Mon, 03 May 1999 11:18:44 +0200 | paulson | renamed state variables | file | diff | annotate |
| Thu, 29 Apr 1999 10:51:58 +0200 | paulson | made many specification operators infix | file | diff | annotate |
| Fri, 27 Nov 1998 17:00:30 +0100 | nipkow | At last: linear arithmetic for nat! | file | diff | annotate |
| Wed, 21 Oct 1998 13:29:01 +0200 | wenzelm | record_split_name; | file | diff | annotate |
| Tue, 20 Oct 1998 17:27:00 +0200 | wenzelm | delSWrapper "record_split_tac"; | file | diff | annotate |
| Thu, 15 Oct 1998 11:35:07 +0200 | paulson | specifications as sets of programs | file | diff | annotate |
| Wed, 07 Oct 1998 10:32:00 +0200 | paulson | tidying and renaming | file | diff | annotate |
| Thu, 01 Oct 1998 18:28:18 +0200 | paulson | abstype of programs | file | diff | annotate |
| Thu, 03 Sep 1998 16:40:02 +0200 | paulson | A new approach, using simp_of_act and simp_of_set to activate definitions when | file | diff | annotate |
| Wed, 02 Sep 1998 10:37:13 +0200 | paulson | modified proofs for new constrains_tac and ensures_tac | file | diff | annotate |
| Wed, 19 Aug 1998 10:34:31 +0200 | paulson | Misc changes | file | diff | annotate |
| Fri, 14 Aug 1998 13:52:42 +0200 | paulson | now trans_tac is part of the claset... | file | diff | annotate |
| Thu, 13 Aug 1998 18:06:40 +0200 | paulson | Constrains, Stable, Invariant...more of the substitution axiom, but Union | file | diff | annotate |
| Thu, 06 Aug 1998 15:47:26 +0200 | paulson | A higher-level treatment of LeadsTo, minimizing use of "reachable" | file | diff | annotate |
| Wed, 05 Aug 1998 10:57:25 +0200 | paulson | New record type of programs | file | diff | annotate |
| Tue, 04 Aug 1998 10:50:33 +0200 | paulson | Constant "invariant" and new constrains_tac, ensures_tac | file | diff | annotate |
| Fri, 31 Jul 1998 18:46:55 +0200 | paulson | Tidied; uses records | file | diff | annotate |
| Thu, 02 Jul 1998 16:53:55 +0200 | paulson | Uncurried functions LeadsTo and reach | file | diff | annotate |
| Mon, 22 Jun 1998 17:26:46 +0200 | wenzelm | isatool fixgoal; | file | diff | annotate |
| Fri, 03 Apr 1998 12:34:33 +0200 | paulson | New UNITY theory | file | diff | annotate |