author | wenzelm |
Wed, 22 Sep 1999 21:04:55 +0200 | |
changeset 7578 | 80525697a87c |
parent 7577 | 644f9b4ae764 |
child 7579 | 20adf381fb0a |
--- 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 "";