# HG changeset patch
# User wenzelm
# Date 938027095 -7200
# Node ID 80525697a87cb450e72573788f41efe48d99e0e9
# Parent  644f9b4ae764afcdca12acdc7fdde1c0b47a8b64
qed "";

diff -r 644f9b4ae764 -r 80525697a87c src/HOL/Isar_examples/Cantor.ML
--- 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 "";