--- a/src/ZF/Trancl.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Trancl.ML Tue Jun 21 17:20:34 1994 +0200
@@ -8,12 +8,6 @@
open Trancl;
-val major::prems = goalw Trancl.thy [trans_def]
- "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
-by (rtac (major RS spec RS spec RS spec RS mp RS mp) 1);
-by (REPEAT (resolve_tac prems 1));
-val transD = result();
-
goal Trancl.thy "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))";
by (rtac bnd_monoI 1);
by (REPEAT (ares_tac [subset_refl, Un_mono, comp_mono] 2));