--- a/thys/Re.thy	Wed Sep 10 12:37:43 2014 +0100
+++ b/thys/Re.thy	Fri Sep 19 12:54:03 2014 +0100
@@ -1,5 +1,5 @@
-(*test*)
-
+(*test*)
+
 theory Re
   imports "Main" 
 begin
@@ -63,6 +63,8 @@
 | "\<turnstile> Void : EMPTY"
 | "\<turnstile> Char c : CHAR c"
 
+thm Prf.intros(1)
+
 section {* The string behind a value *}
 
 fun flat :: "val \<Rightarrow> string"