qed "";
authorwenzelm
Wed Sep 22 21:04:55 1999 +0200 (1999-09-22)
changeset 757880525697a87c
parent 7577 644f9b4ae764
child 7579 20adf381fb0a
qed "";
src/HOL/Isar_examples/Cantor.ML
     1.1 --- a/src/HOL/Isar_examples/Cantor.ML	Wed Sep 22 21:04:34 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/Cantor.ML	Wed Sep 22 21:04:55 1999 +0200
     1.3 @@ -10,11 +10,11 @@
     1.4    by (contr_tac 1);
     1.5    by (swap_res_tac [CollectI] 1);
     1.6    by (assume_tac 1);
     1.7 -qed "it";
     1.8 +qed "";
     1.9  
    1.10  
    1.11  (* tactic script -- automatic *)
    1.12  
    1.13  Goal "EX S. S ~: range(f :: 'a => 'a set)";
    1.14    by (best_tac (claset() addSEs [equalityCE]) 1);
    1.15 -qed "it";
    1.16 +qed "";