src/HOL/Isar_examples/Cantor.ML
author wenzelm
Wed, 22 Sep 1999 21:04:55 +0200
changeset 7578 80525697a87c
parent 7322 d16d7ddcc842
child 9474 b0ce3b7c9c26
permissions -rw-r--r--
qed "";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6516
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
     1
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
     2
(* tactic script -- single steps *)
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
     3
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
     4
Goal "EX S. S ~: range(f :: 'a => 'a set)";
7322
d16d7ddcc842 isatool expandshort;
wenzelm
parents: 6516
diff changeset
     5
  by (rtac exI 1);
d16d7ddcc842 isatool expandshort;
wenzelm
parents: 6516
diff changeset
     6
  by (rtac notI 1);
d16d7ddcc842 isatool expandshort;
wenzelm
parents: 6516
diff changeset
     7
  by (etac rangeE 1);
d16d7ddcc842 isatool expandshort;
wenzelm
parents: 6516
diff changeset
     8
  by (etac equalityCE 1);
d16d7ddcc842 isatool expandshort;
wenzelm
parents: 6516
diff changeset
     9
  by (dtac CollectD 1);
6516
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
    10
  by (contr_tac 1);
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
    11
  by (swap_res_tac [CollectI] 1);
7322
d16d7ddcc842 isatool expandshort;
wenzelm
parents: 6516
diff changeset
    12
  by (assume_tac 1);
7578
80525697a87c qed "";
wenzelm
parents: 7322
diff changeset
    13
qed "";
6516
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
    14
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
    15
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
    16
(* tactic script -- automatic *)
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
    17
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
    18
Goal "EX S. S ~: range(f :: 'a => 'a set)";
09207771cc7c added Isar_examples/Cantor.ML;
wenzelm
parents:
diff changeset
    19
  by (best_tac (claset() addSEs [equalityCE]) 1);
7578
80525697a87c qed "";
wenzelm
parents: 7322
diff changeset
    20
qed "";