# HG changeset patch
# User huffman
# Date 1321357189 -3600
# Node ID 44790ec65f70ccc964ca754b22e7c4690dcf5b0c
# Parent  6246bef495ff5c119b986d2c36967861d9178036
remove old-style semicolons

diff -r 6246bef495ff -r 44790ec65f70 src/HOL/Metis_Examples/Abstraction.thy
--- 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 (simp add: );
+apply (clarify )
+apply (simp add: )
 apply (rule rev_image_eqI)
-apply (blast intro: elim:);
-apply (simp add: );
+apply (blast intro: elim:)
+apply (simp add: )
 done
 
 (*Given the difficulty of the previous problem, these two are probably
diff -r 6246bef495ff -r 44790ec65f70 src/HOL/Metis_Examples/Message.thy
--- 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