# HG changeset patch # User haftmann # Date 1223388460 -7200 # Node ID 5818d9cfb2e78a7c2b839ca57206281efe37db87 # Parent eacb54d9e78d1d5af9dc13c96faf0faa8ddfd26e tuned whitespace diff -r eacb54d9e78d -r 5818d9cfb2e7 src/HOL/ex/Efficient_Nat_examples.thy --- a/src/HOL/ex/Efficient_Nat_examples.thy Tue Oct 07 16:07:33 2008 +0200 +++ b/src/HOL/ex/Efficient_Nat_examples.thy Tue Oct 07 16:07:40 2008 +0200 @@ -3,7 +3,7 @@ Author: Florian Haftmann, TU Muenchen *) -header {* Simple examples for Efficient\_Nat theory. *} +header {* Simple examples for Efficient\_Nat theory. *} theory Efficient_Nat_examples imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat