fixed goal selection;

--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Apr 05 21:06:06 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Apr 05 21:06:37 2000 +0200
@@ -274,8 +274,8 @@
       have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
         < card (?e ?t' 0)";
       proof (rule card_Diff1_less);
-	show "finite (?e ?t' 0)";
-          by (rule finite_subset, rule fin) force;
+	from _ fin; show "finite (?e ?t' 0)";
+          by (rule finite_subset) force;
 	show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0"; by simp;
       qed;
       thus ?thesis; by simp;

--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Apr 05 21:06:06 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Apr 05 21:06:37 2000 +0200
@@ -72,14 +72,14 @@
         qed;
         show "is_linearform ?H ?h"; 
           by (simp! add: sup_lf a);
-        show "is_subspace ?H E"; 
-          by (rule sup_subE, rule a) (simp!)+;
+        show "is_subspace ?H E";
+          by (rule sup_subE [OF _ _ _ a]) (simp!)+;
         show "is_subspace F ?H"; 
-          by (rule sup_supF, rule a) (simp!)+;
+          by (rule sup_supF [OF _ _ _ a]) (simp!)+;
         show "graph F f <= graph ?H ?h"; 
-          by (rule sup_ext, rule a) (simp!)+;
+          by (rule sup_ext [OF _ _ _ a]) (simp!)+;
         show "ALL x::'a:?H. ?h x <= p x"; 
-          by (rule sup_norm_pres, rule a) (simp!)+;
+          by (rule sup_norm_pres [OF _ _ a]) (simp!)+;
       qed;
     qed;
   }};
@@ -190,7 +190,7 @@
 
 txt {* Define the extension $h_0$ of $h$ to $H_0$ using $\xi$.  *};
 
-            def h0 == "\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 
+            def h0 == "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 
                                                   & y:H
                            in (h y) + a * xi";
             show ?thesis;
@@ -205,9 +205,9 @@
 		  have  "graph H h <= graph H0 h0";
                   proof (rule graph_extI);
 		    fix t; assume "t:H"; 
-		    have "(SOME (y, a). t = y + a <*> x0 & y : H) 
+		    have "(SOME (y, a). t = y + a <*> x0 & y : H)
                          = (t,0r)";
-		      by (rule decomp_H0_H, rule x0); 
+		      by (rule decomp_H0_H [OF _ _ _ _ _ x0]);
 		    thus "h t = h0 t"; by (simp! add: Let_def);
 		  next;
 		    show "H <= H0";
@@ -248,10 +248,9 @@
 		have "graph H0 h0 : norm_pres_extensions E p F f";
 		proof (rule norm_pres_extensionI2);
 		  show "is_linearform H0 h0";
-		    by (rule h0_lf, rule x0) (simp!)+;
+		    by (rule h0_lf [OF _ _ _ _ _ _ x0]) (simp!)+;
 		  show "is_subspace H0 E";
-		    by (unfold H0_def, rule vs_sum_subspace, 
-                        rule lin_subspace);
+		    by (unfold H0_def) (rule vs_sum_subspace [OF _ lin_subspace]);
 		  have "is_subspace F H"; .;
 		  also; from h lin_vs; 
 		  have [fold H0_def]: "is_subspace H (H + lin x0)"; ..;
@@ -267,7 +266,7 @@
 		      by (simp add: Let_def);
 		    also; have 
 		      "(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)";
-		      by (rule decomp_H0_H [RS sym], rule x0) (simp!)+;
+		      by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x0]) (simp!)+;
 		    also; have 
 		      "(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H)
                         in h y + a * xi) 
@@ -278,7 +277,7 @@
 		  qed;
 		
 		  show "ALL x:H0. h0 x <= p x";
-		    by (rule h0_norm_pres, rule x0);
+		    by (rule h0_norm_pres [OF _ _ _ _ x0]);
 		qed;
 		thus "graph H0 h0 : M"; by (simp!);
 	      qed;
@@ -472,7 +471,7 @@
       of $h$ on $H_0$:*};  
 
       def h0 ==
-          "\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 & y:H
+          "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 & y:H
                in (h y) + a * xi";
 
       txt {* We get that the graph of $h_0$ extends that of
@@ -655,7 +654,7 @@
   \end{matharray}
   *};
 
-  def p == "\<lambda>x. function_norm F norm f * norm x";
+  def p == "\\<lambda>x. function_norm F norm f * norm x";
   
   txt{* $p$ is a seminorm on $E$: *};
 

--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Wed Apr 05 21:06:06 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Wed Apr 05 21:06:37 2000 +0200
@@ -32,7 +32,7 @@
   assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M"
      and u: "graph H h = Union c" "x:H";
 
-  let ?P = "\<lambda>H h. is_linearform H h
+  let ?P = "\\<lambda>H h. is_linearform H h
                 & is_subspace H E
                 & is_subspace F H
                 & graph F f <= graph H h
@@ -273,7 +273,7 @@
   assume "M = norm_pres_extensions E p F f" "c: chain M" 
          "graph H h = Union c";
  
-  let ?P = "\<lambda>H h. is_linearform H h 
+  let ?P = "\\<lambda>H h. is_linearform H h 
                 & is_subspace H E 
                 & is_subspace F H
                 & graph F f <= graph H h
@@ -677,8 +677,8 @@
 	from h; have "- h x = h (- x)"; 
           by (rule linearform_neg [RS sym]);
 	also; from r; have "... <= p (- x)"; by (simp!);
-	also; have "... = p x"; 
-          by (rule seminorm_minus, rule subspace_subsetD);
+	also; have "... = p x";
+          by (rule seminorm_minus [OF _ subspace_subsetD]);
 	finally; show "- h x <= p x"; .; 
       qed;
       from r; show "h x <= p x"; ..;