summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 30 Jul 2000 13:02:56 +0200 | |

changeset 9474 | b0ce3b7c9c26 |

parent 9473 | 7d13a5ace928 |

child 9475 | b24516d96847 |

removed equalityCE;

src/HOL/Isar_examples/Cantor.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Isar_examples/Cantor.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Isar_examples/Cantor.ML Sun Jul 30 13:02:14 2000 +0200 +++ b/src/HOL/Isar_examples/Cantor.ML Sun Jul 30 13:02:56 2000 +0200 @@ -1,7 +1,7 @@ (* tactic script -- single steps *) -Goal "EX S. S ~: range(f :: 'a => 'a set)"; +Goal "EX S. S ~: range (f :: 'a => 'a set)"; by (rtac exI 1); by (rtac notI 1); by (etac rangeE 1); @@ -15,6 +15,6 @@ (* tactic script -- automatic *) -Goal "EX S. S ~: range(f :: 'a => 'a set)"; - by (best_tac (claset() addSEs [equalityCE]) 1); +Goal "EX S. S ~: range (f :: 'a => 'a set)"; + by (Best_tac 1); qed "";

--- a/src/HOL/Isar_examples/Cantor.thy Sun Jul 30 13:02:14 2000 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Sun Jul 30 13:02:56 2000 +0200 @@ -95,16 +95,15 @@ text {* How much creativity is required? As it happens, Isabelle can prove - this theorem automatically. The context of Isabelle's classical - prover contains rules for most of the constructs of HOL's set theory. - We must augment it with \name{equalityCE} to break up set equalities, - and then apply best-first search. Depth-first search would diverge, - but best-first search successfully navigates through the large search - space. + this theorem automatically using best-first search. Depth-first + search would diverge, but best-first search successfully navigates + through the large search space. The context of Isabelle's classical + prover contains rules for the relevant constructs of HOL's set + theory. *}; theorem "EX S. S ~: range (f :: 'a => 'a set)"; - by (best elim: equalityCE); + by best; text {* While this establishes the same theorem internally, we do not get any