--- a/src/ZF/ex/Data.ML Mon Jun 22 17:12:27 1998 +0200
+++ b/src/ZF/ex/Data.ML Mon Jun 22 17:13:09 1998 +0200
@@ -9,7 +9,7 @@
open Data;
-goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
+Goal "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
let open data; val rew = rewrite_rule con_defs in
by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
end;
@@ -17,13 +17,13 @@
(** Lemmas to justify using "data" in other recursive type definitions **)
-goalw Data.thy data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
+Goalw data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
by (rtac lfp_mono 1);
by (REPEAT (rtac data.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1));
qed "data_mono";
-goalw Data.thy (data.defs@data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
+Goalw (data.defs@data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2);
by (fast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,