Fri, 26 May 1995 18:11:47 +0200 | nipkow | Trancl is now based on Relation which used to be in Integ. | changeset | files |
Fri, 26 May 1995 11:20:08 +0200 | wenzelm | changed macro expander such that patterns also match prefixes of appls; | changeset | files |
Mon, 22 May 1995 16:00:26 +0200 | nipkow | Moved comment from ParRed.thy to ROOT.ML | changeset | files |
Mon, 22 May 1995 15:58:57 +0200 | nipkow | Added Park induction to Lfp. | changeset | files |
Mon, 22 May 1995 14:12:40 +0200 | nipkow | Polished the presentation making it completely definitional. | changeset | files |
Thu, 18 May 1995 11:51:23 +0200 | lcp | Krzysztof Grabczewski's (nearly) complete AC proofs | changeset | files |
Mon, 15 May 1995 09:35:07 +0200 | nipkow | renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans. | changeset | files |
Sat, 13 May 1995 14:08:24 +0200 | nipkow | Added some lemmas about r^*. | changeset | files |