src/HOL/ex/Recdef.ML

--- a/src/HOL/ex/Recdef.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/ex/Recdef.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -11,7 +11,7 @@
 
 Addsimps qsort.rules;
 
-goal thy "(x mem qsort (ord,l)) = (x mem l)";
+Goal "(x mem qsort (ord,l)) = (x mem l)";
 by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
@@ -22,13 +22,13 @@
 
 Addsimps g.rules;
 
-goal thy "g x < Suc x";
+Goal "g x < Suc x";
 by (res_inst_tac [("u","x")] g.induct 1);
 by Auto_tac;
 by (trans_tac 1);
 qed "g_terminates";
 
-goal thy "g x = 0";
+Goal "g x = 0";
 by (res_inst_tac [("u","x")] g.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
 qed "g_zero";