From 5ae63c07a6d8e53dcf9bf2a542a8f3c28ee66ceb Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 16 May 2015 17:53:25 +1000 Subject: [PATCH] fix(doc/lean/library_style.org): remove unnecessary header line --- doc/lean/library_style.org | 2 -- 1 file changed, 2 deletions(-) diff --git a/doc/lean/library_style.org b/doc/lean/library_style.org index e283a10be..3729256ec 100644 --- a/doc/lean/library_style.org +++ b/doc/lean/library_style.org @@ -1,8 +1,6 @@ #+Title: Library Style Guidelines #+Author: [[http://www.andrew.cmu.edu/user/avigad][Jeremy Avigad]] -* Library Style Guidelines - Files in the Lean library generally adhere to the following guidelines and conventions. Having a uniform style makes it easier to browse the library and read the contents, but these are meant to be guidelines