author huffman Tue, 15 Nov 2011 12:39:49 +0100 changeset 45503 44790ec65f70 parent 45502 6246bef495ff child 45504 cad35ed6effa
remove old-style semicolons
```--- a/src/HOL/Metis_Examples/Abstraction.thy	Tue Nov 15 12:39:29 2011 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Tue Nov 15 12:39:49 2011 +0100
@@ -14,7 +14,7 @@
declare [[metis_new_skolemizer]]

(*For Christoph Benzmueller*)
-lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))";
+lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))"
by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)

(*this is a theorem, but we can't prove it unless ext is applied explicitly
@@ -182,7 +182,7 @@

declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenB" ]]
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A
-       ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
+       ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
by (metis Collect_def imageI image_image image_subset_iff mem_def)

declare [[ sledgehammer_problem_prefix = "Abstraction__image_curry" ]]
@@ -208,11 +208,11 @@
apply (rule SigmaI)
apply (erule imageI) +
txt{*subgoal 2*}
-apply (clarify );
+apply (clarify )
apply (rule rev_image_eqI)
-apply (blast intro: elim:);
+apply (blast intro: elim:)
done

(*Given the difficulty of the previous problem, these two are probably```
```--- a/src/HOL/Metis_Examples/Message.thy	Tue Nov 15 12:39:29 2011 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Tue Nov 15 12:39:49 2011 +0100
@@ -243,7 +243,7 @@
done

lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
-by (blast dest: parts_mono);
+by (blast dest: parts_mono)

lemma parts_cut: "[|Y\<in> parts (insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
@@ -665,7 +665,7 @@
done

lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
-apply (rule equalityI);
+apply (rule equalityI)
apply (metis analz_idem analz_subset_cong order_eq_refl)
apply (metis analz_increasing analz_subset_cong order_eq_refl)
done```