src/HOL/Isar_examples/Cantor.ML
changeset 7578 80525697a87c
parent 7322 d16d7ddcc842
child 9474 b0ce3b7c9c26
--- a/src/HOL/Isar_examples/Cantor.ML	Wed Sep 22 21:04:34 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.ML	Wed Sep 22 21:04:55 1999 +0200
@@ -10,11 +10,11 @@
   by (contr_tac 1);
   by (swap_res_tac [CollectI] 1);
   by (assume_tac 1);
-qed "it";
+qed "";
 
 
 (* tactic script -- automatic *)
 
 Goal "EX S. S ~: range(f :: 'a => 'a set)";
   by (best_tac (claset() addSEs [equalityCE]) 1);
-qed "it";
+qed "";