# HG changeset patch # User krauss # Date 1286956560 -7200 # Node ID 8a2c7547835728ac3e2ff662c1e6762d88d60016 # Parent 9b4341366b63af4d63ceb44f6bcb4d0a09319fa2 reactivated diff -r 9b4341366b63 -r 8a2c75478357 src/ZF/ex/misc.thy --- a/src/ZF/ex/misc.thy Tue Oct 12 21:30:44 2010 +0200 +++ b/src/ZF/ex/misc.thy Wed Oct 13 09:56:00 2010 +0200 @@ -39,19 +39,19 @@ lemma "(X = Y Un Z) <-> (Y \ X & Z \ X & (\V. Y \ V & Z \ V --> X \ V))" by (blast intro!: equalityI) -text{*the dual of the previous one} +text{*the dual of the previous one*} lemma "(X = Y Int Z) <-> (X \ Y & X \ Z & (\V. V \ Y & V \ Z --> V \ X))" by (blast intro!: equalityI) -text{*trivial example of term synthesis: apparently hard for some provers!} -lemma "a \ b ==> a:?X & b \ ?X" +text{*trivial example of term synthesis: apparently hard for some provers!*} +schematic_lemma "a \ b ==> a:?X & b \ ?X" by blast -text{*Nice Blast_tac benchmark. Proved in 0.3s; old tactics can't manage it!} +text{*Nice blast benchmark. Proved in 0.3s; old tactics can't manage it!*} lemma "\x \ S. \y \ S. x \ y ==> \z. S \ {z}" by blast -text{*variant of the benchmark above} +text{*variant of the benchmark above*} lemma "\x \ S. Union(S) \ x ==> \z. S \ {z}" by blast @@ -74,7 +74,7 @@ Set Theory in First-Order Logic: Clauses for G\"odel's Axioms, JAR 2 (1986), 287-327 *} -text{*collecting the relevant lemmas} +text{*collecting the relevant lemmas*} declare comp_fun [simp] SigmaI [simp] apply_funtype [simp] (*Force helps prove conditions of rewrites such as comp_fun_apply, since @@ -86,7 +86,7 @@ (K O J) \ hom(A,f,C,h)" by force -text{*Another version, with meta-level rewriting} +text{*Another version, with meta-level rewriting*} lemma "(!! A f B g. hom(A,f,B,g) == {H \ A->B. f \ A*A->A & g \ B*B->B & (\x \ A. \y \ A. H`(f`) = g`)}) @@ -108,7 +108,7 @@ "[| (h O g O f) \ inj(A,A); (f O h O g) \ surj(B,B); (g O f O h) \ surj(C,C); - f \ A->B; g \ B->C; h \ C->A |] ==> h \ bij(C,A)"; + f \ A->B; g \ B->C; h \ C->A |] ==> h \ bij(C,A)" by (unfold bij_def, blast) lemma pastre3: