Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove one more old-style semicolon
authorhuffman
Tue, 15 Nov 2011 12:51:14 +0100
changeset 45505 dc452a1a46e5
parent 45504 cad35ed6effa
child 45506 4cc83e901acf
child 45528 726b743855ea
remove one more old-style semicolon
src/HOL/Metis_Examples/Message.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Metis_Examples/Message.thy	Tue Nov 15 12:49:05 2011 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Tue Nov 15 12:51:14 2011 +0100
@@ -738,7 +738,7 @@
 
 lemma Fake_parts_insert_in_Un:
      "[|Z \<in> parts (insert X H);  X: synth (analz H)|]
-      ==> Z \<in>  synth (analz H) \<union> parts H";
+      ==> Z \<in>  synth (analz H) \<union> parts H"
 by (blast dest: Fake_parts_insert [THEN subsetD, dest])
 
 declare analz_mono [intro] synth_mono [intro]
isabelle