diff -r dfa9dbb8f8e6 -r f95a405c3180 thys/notes.tex
--- a/thys/notes.tex	Fri Mar 13 21:27:03 2015 +0000
+++ b/thys/notes.tex	Fri Apr 10 22:38:36 2015 +0100
@@ -435,9 +435,7 @@
       Many of such rule are called intro-rules and end with 
       an ``$I$'', or in case of inductive predicates $\_.intros$.
       
-      
-       
-       
+   
 \end{itemize}