# HG changeset patch
# User wenzelm
# Date 1001706340 -7200
# Node ID 4213422388c436eeac53b66aa76e04c814e6e7af
# Parent  2c3dee321b4b0faa0f4d8bdc144c6da64f9b128c
tuned;

diff -r 2c3dee321b4b -r 4213422388c4 src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Fri Sep 28 21:45:11 2001 +0200
+++ b/src/HOL/Lambda/InductTermi.thy	Fri Sep 28 21:45:40 2001 +0200
@@ -114,4 +114,4 @@
    apply force
    done
 
-end
\ No newline at end of file
+end
diff -r 2c3dee321b4b -r 4213422388c4 src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Fri Sep 28 21:45:11 2001 +0200
+++ b/src/HOL/Lambda/ListBeta.thy	Fri Sep 28 21:45:40 2001 +0200
@@ -109,4 +109,4 @@
   apply blast
   done
 
-end
\ No newline at end of file
+end
diff -r 2c3dee321b4b -r 4213422388c4 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Fri Sep 28 21:45:11 2001 +0200
+++ b/src/HOL/Lambda/ListOrder.thy	Fri Sep 28 21:45:40 2001 +0200
@@ -121,4 +121,4 @@
   apply blast
   done
 
-end
\ No newline at end of file
+end