src/HOL/Ord.ML

 The type class for ordered types
 *)
 
 (** mono **)
 
-val [prem] = goalw Ord.thy [mono_def]
+val [prem] = Goalw [mono_def]
     "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
 by (REPEAT (ares_tac [allI, impI, prem] 1));
 qed "monoI";
 
-val [major,minor] = goalw Ord.thy [mono_def]
-    "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
-by (rtac (major RS spec RS spec RS mp) 1);
-by (rtac minor 1);
+Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
+by (Fast_tac 1);
 qed "monoD";
 
 
 section "Orders";
 

 
 val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
 by (simp_tac (simpset() addsimps prems) 1);
 qed "min_leastL";
 
-val prems = goalw thy [min_def]
+val prems = Goalw [min_def]
  "(!!x::'a::order. least <= x) ==> min x least = least";
 by (cut_facts_tac prems 1);
 by (Asm_simp_tac 1);
 by (blast_tac (claset() addIs [order_antisym]) 1);
 qed "min_leastR";