paulson [Mon, 17 Aug 1998 13:09:08 +0200] rev 5325
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
contains fewer theorems than before
paulson [Mon, 17 Aug 1998 13:06:29 +0200] rev 5324
Now allows "." in rule names, with special treatment for "be"
nipkow [Mon, 17 Aug 1998 11:00:57 +0200] rev 5323
Direct translation RegExp -> NA!
nipkow [Mon, 17 Aug 1998 11:00:27 +0200] rev 5322
Additions to Lex.
paulson [Fri, 14 Aug 1998 18:37:28 +0200] rev 5321
got rid of some goal thy commands
paulson [Fri, 14 Aug 1998 13:52:42 +0200] rev 5320
now trans_tac is part of the claset...
paulson [Fri, 14 Aug 1998 12:06:34 +0200] rev 5319
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson [Fri, 14 Aug 1998 12:03:01 +0200] rev 5318
expandshort
paulson [Fri, 14 Aug 1998 12:02:35 +0200] rev 5317
Uses Goal instead of "goal...thy" to avoid theory problems
paulson [Thu, 13 Aug 1998 18:14:26 +0200] rev 5316
even more tidying of Goal commands