src/ZF/OrderArith.ML

 
 goalw OrderArith.thy [radd_def] "radd(A,r,B,s) <= (A+B) * (A+B)";
 by (rtac Collect_subset 1);
 qed "radd_type";
 
-val field_radd = standard (radd_type RS field_rel_subset);
+bind_thm ("field_radd", (radd_type RS field_rel_subset));
 
 (** Linearity **)
 
 val radd_ss = sum_ss addsimps [radd_Inl_iff, radd_Inr_iff, 
 			       radd_Inl_Inr_iff, radd_Inr_Inl_iff];

 
 goalw OrderArith.thy [rmult_def] "rmult(A,r,B,s) <= (A*B) * (A*B)";
 by (rtac Collect_subset 1);
 qed "rmult_type";
 
-val field_rmult = standard (rmult_type RS field_rel_subset);
+bind_thm ("field_rmult", (rmult_type RS field_rel_subset));
 
 (** Linearity **)
 
 val [lina,linb] = goal OrderArith.thy
     "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))";

 
 goalw OrderArith.thy [rvimage_def] "rvimage(A,f,r) <= A*A";
 by (rtac Collect_subset 1);
 qed "rvimage_type";
 
-val field_rvimage = standard (rvimage_type RS field_rel_subset);
+bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset));
 
 
 (** Linearity **)
 
 val [finj,lin] = goalw OrderArith.thy [inj_def]