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

author | wenzelm |

Tue, 27 Apr 1999 10:46:37 +0200 | |

changeset 6517 | 239c0eff6ce8 |

parent 6516 | 09207771cc7c |

child 6518 | e9d6f165f9c1 |

tuned;

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

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

--- a/src/HOL/Isar_examples/Cantor.thy Tue Apr 27 10:45:20 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Tue Apr 27 10:46:37 1999 +0200 @@ -9,7 +9,7 @@ theory Cantor = Main:; -section "Example: Cantor's Theorem" +section "Example: Cantor's Theorem"; text {| Cantor's Theorem states that every set has more subsets than it has @@ -23,14 +23,14 @@ The Isabelle/Isar proofs below use HOL's set theory, with the type @{type "'a set"} and the operator @{term range}. -|} +|}; text {| We first consider a rather verbose version of the proof, with the reasoning expressed quite naively. We only make use of the pure core of the Isar proof language. -|} +|}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; proof; @@ -63,7 +63,7 @@ The following version essentially does the same reasoning, only that it is expressed more neatly, with some derived Isar language elements involved. -|} +|}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; proof; @@ -98,7 +98,7 @@ then apply best-first search. Depth-first search would diverge, but best-first search successfully navigates through the large search space. -|} +|}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; by (best elim: equalityCE); @@ -109,7 +109,7 @@ to transform internal system-level representations of Isabelle proofs back into Isar documents. Writing Isabelle/Isar proof documents actually \emph{is} a creative process. -|} +|}; end;

--- a/src/HOL/Isar_examples/ExprCompiler.thy Tue Apr 27 10:45:20 1999 +0200 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Tue Apr 27 10:46:37 1999 +0200 @@ -101,7 +101,6 @@ @{term "comp"}. We first establish some lemmas. |}; -ML "reset HOL_quantifiers"; lemma exec_append: "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");