From 6eb7d1cde30e83f9d54e348721f1dedd4b427cf9 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Sat, 2 Apr 2022 13:12:59 +0100
Subject: [PATCH] Renaming to comply with the usual naming convention that
 theory names start with an uppercase letter.

---
 fxp.thy => Fxp.thy                 |  2 +-
 ml_yacc_lib.thy => Ml_Yacc_Lib.thy |  2 +-
 README.md                          | 20 ++++++++++----------
 ROOT                               |  8 ++++----
 4 files changed, 16 insertions(+), 16 deletions(-)
 rename fxp.thy => Fxp.thy (99%)
 rename ml_yacc_lib.thy => Ml_Yacc_Lib.thy (99%)

diff --git a/fxp.thy b/Fxp.thy
similarity index 99%
rename from fxp.thy
rename to Fxp.thy
index 024ac50..ffa2f34 100644
--- a/fxp.thy
+++ b/Fxp.thy
@@ -44,7 +44,7 @@ to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 ***********************************************************************************)
 
 chapter\<open>The Functional XML Parser for Isabelle\<close>
-theory fxp
+theory Fxp
   imports Main 
 begin 
 
diff --git a/ml_yacc_lib.thy b/Ml_Yacc_Lib.thy
similarity index 99%
rename from ml_yacc_lib.thy
rename to Ml_Yacc_Lib.thy
index 3e69e0c..e3d8377 100644
--- a/ml_yacc_lib.thy
+++ b/Ml_Yacc_Lib.thy
@@ -45,7 +45,7 @@ to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
 chapter\<open>ML Yacc Library for Isabelle\<close>
 theory
-  "ml_yacc_lib"
+  "Ml_Yacc_Lib"
   imports
   Main
 begin
diff --git a/README.md b/README.md
index c943e97..c71ab76 100644
--- a/README.md
+++ b/README.md
@@ -14,6 +14,13 @@ older versions might be available on a dedicated branch.
   that provides a simple way for specifying assertions that Isabelle
   checks while processing a theory.
 
+* [Code_Reflection.thy](Code_Reflection.thy) provides a new top-level 
+  command for reflecting generated SML code into Isabelle's ML 
+  environment.
+
+* [Fxp.thy](Fxp.thy) provides Isabelle support for The Functional XML
+  Parser (fxp).
+
 * [Hiding_Type_Variables.thy](Hiding_Type_Variables.thy) provides
   print a setup for defining default type variables of type
   constructors. The default type variables can be hidden in output,
@@ -22,18 +29,11 @@ older versions might be available on a dedicated branch.
   which (sometimes) helps to focus on the important parts of complex
   type declarations.
 
-* [Nano_JSON.thy](Nano_JSON.thy) provides support for a JSON-like 
-  data exchange for Isabelle/HOL.
-
-* [Code_Reflection.thy](Code_Reflection.thy) provides a new top-level 
-  command for reflecting generated SML code into Isabelle's ML 
-  environment.
-
-* [ml_yacc_lib.thy](ml_yacc_lib.thy) provides Isabelle support for parser 
+* [Ml_Yacc_Lib.thy](Ml_Yacc_Lib.thy) provides Isabelle support for parser 
   generated by ml-yacc (part of sml/NJ).
 
-* [fxp.thy](fxp.thy) provides Isabelle support for The Functional XML
-  Parser (fxp).
+* [Nano_JSON.thy](Nano_JSON.thy) provides support for a JSON-like 
+  data exchange for Isabelle/HOL.
 
 * [Simple_Oracle.thy](Simple_Oracle.thy) provides an example on integrating 
   an external tool as simple oracle or counter example generator, similar
diff --git a/ROOT b/ROOT
index 92755d5..68035d3 100644
--- a/ROOT
+++ b/ROOT
@@ -2,11 +2,11 @@ session "isabelle-hacks" = "HOL" +
   options [timeout = 600, document = pdf, document_variants="document:outline=/proof,/ML",document_output=output]
   theories
     Assert
-    Hiding_Type_Variables
-    Nano_JSON
     Code_Reflection
-    fxp
-    ml_yacc_lib 
+    Fxp
+    Hiding_Type_Variables
+    Ml_Yacc_Lib 
+    Nano_JSON
     Simple_Oracle
   document_files
     root.tex