# HG changeset patch
# User berghofe
# Date 1275383620 -7200
# Node ID 95bfc649fe199a9d9f88ac9828a278be8758221c
# Parent  b78f31ca46754fb71a4886c8c39848ab5663a817
Tuned.

diff -r b78f31ca4675 -r 95bfc649fe19 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Tue Jun 01 11:13:09 2010 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue Jun 01 11:13:40 2010 +0200
@@ -264,6 +264,7 @@
 lemmas [extraction_expand] = conj_assoc listall_cons_eq
 
 extract type_NF
+
 lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
   apply (rule iffI)
   apply (erule rtranclpR.induct)