src/HOL/Trancl.ML
Mon, 23 Jun 1997 10:42:03 +0200 paulson Ran expandshort
Tue, 17 Jun 1997 09:01:56 +0200 nipkow converse -> ^-1
Thu, 05 Jun 1997 14:39:22 +0200 nipkow Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
Fri, 11 Apr 1997 15:21:36 +0200 paulson Yet more fast_tac->blast_tac, and other tidying
Wed, 09 Apr 1997 12:32:04 +0200 paulson Using Blast_tac
Fri, 04 Apr 1997 11:18:52 +0200 paulson Calls Blast_tac
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Thu, 12 Sep 1996 10:40:05 +0200 paulson Tidied many proofs, using AddIffs to let equivalences take
Mon, 19 Aug 1996 13:03:17 +0200 paulson Tidied up the proofs
Mon, 03 Jun 1996 17:10:56 +0200 berghofe best_tac, deepen_tac and safe_tac now also use default claset.
Fri, 24 May 1996 11:48:18 +0200 nipkow Modified proof of "(R^=)^* = R^*" to accommodate equalityI.
Thu, 23 May 1996 14:37:06 +0200 berghofe Replaced fast_tac by Fast_tac (which uses default claset)
Fri, 17 May 1996 12:23:44 +0200 nipkow Moved split_rule et al from ind_syntax.ML to Prod.ML.
Tue, 30 Apr 1996 17:30:54 +0200 nipkow Added backwards rtrancl_induct and special versions for pairs.
Thu, 04 Apr 1996 11:45:01 +0200 paulson Using new "Times" infix
Wed, 06 Mar 1996 12:52:11 +0100 paulson Ran expandshort
Thu, 15 Feb 1996 08:10:36 +0100 nipkow Added a few thms and the new theory RelPow.
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Wed, 25 Oct 1995 09:48:29 +0100 nipkow Added various thms and tactics.
Sun, 28 May 1995 17:17:43 +0200 nipkow Added trancl_cs
Fri, 26 May 1995 18:11:47 +0200 nipkow Trancl is now based on Relation which used to be in Integ.
Mon, 15 May 1995 09:35:07 +0200 nipkow renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans.
Sat, 13 May 1995 14:08:24 +0200 nipkow Added some lemmas about r^*.
Fri, 24 Mar 1995 12:30:35 +0100 clasohm changed syntax of tuples from <..., ...> to (..., ...)
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application
less more (0) tip