src/HOL/UNITY/Lift.ML
Fri, 07 May 1999 10:50:28 +0200 paulson tidied
Tue, 04 May 1999 10:26:00 +0200 paulson Invariant -> Always and other tidying
Thu, 29 Apr 1999 10:51:58 +0200 paulson made many specification operators infix
Fri, 29 Jan 1999 16:23:56 +0100 paulson tidied
Tue, 19 Jan 1999 11:16:07 +0100 paulson simplified thanks to the arithmetic prover
Thu, 14 Jan 1999 14:39:11 +0100 nipkow Removed superfluous arith rules from metric_simps
Thu, 14 Jan 1999 13:18:09 +0100 nipkow More arith refinements.
Tue, 05 Jan 1999 17:28:34 +0100 nipkow 1 proof now automatic.
Fri, 11 Dec 1998 10:41:53 +0100 paulson new Close_locale synatx
Sat, 31 Oct 1998 12:43:56 +0100 paulson no need for int_0
Fri, 23 Oct 1998 20:44:34 +0200 oheimb corrected auto_tac (applications of unsafe wrappers)
Wed, 21 Oct 1998 13:29:01 +0200 wenzelm record_split_name;
Tue, 20 Oct 1998 17:27:00 +0200 wenzelm delSWrapper "record_split_tac";
Thu, 15 Oct 1998 11:35:07 +0200 paulson specifications as sets of programs
Thu, 01 Oct 1998 18:28:18 +0200 paulson abstype of programs
Tue, 29 Sep 1998 15:58:25 +0200 paulson modified proof for new simproc
Fri, 25 Sep 1998 13:58:24 +0200 paulson Now uses integers instead of naturals
Tue, 15 Sep 1998 15:04:07 +0200 paulson From Compl(A) to -A
Mon, 14 Sep 1998 10:17:44 +0200 paulson simpler proof
Fri, 11 Sep 1998 18:09:54 +0200 paulson Extra steps at end to make it run faster
Fri, 11 Sep 1998 16:25:40 +0200 paulson fixed PROOF FAILED
Thu, 03 Sep 1998 16:40:02 +0200 paulson A new approach, using simp_of_act and simp_of_set to activate definitions when
Wed, 02 Sep 1998 10:37:13 +0200 paulson modified proofs for new constrains_tac and ensures_tac
Tue, 01 Sep 1998 10:10:11 +0200 paulson Moved lemmas to Arith.ML
Thu, 20 Aug 1998 17:43:01 +0200 paulson New theory Lift
Wed, 19 Aug 1998 10:34:31 +0200 paulson Misc changes
Fri, 14 Aug 1998 13:52:42 +0200 paulson now trans_tac is part of the claset...
Thu, 13 Aug 1998 18:06:40 +0200 paulson Constrains, Stable, Invariant...more of the substitution axiom, but Union
Thu, 06 Aug 1998 15:47:26 +0200 paulson A higher-level treatment of LeadsTo, minimizing use of "reachable"
less more (0) tip