Update documentation structure

Huub Vromen · Huub Vromen · commit dd11e80b65a9 · 2025-11-28T13:31:20.000+01:00
diff --git a/LICENSE b/LICENSE
@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2024 Huub Vromen
+Copyright (c) 2025 Huub Vromen
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal
diff --git a/Main.lean b/Main.lean
diff --git a/README.md b/README.md
@@ -35,13 +35,12 @@ All proofs are fully formalized and verified in Lean 4 with **zero `sorry` state
 ├── LICENSE                            # MIT License
 ├── lakefile.lean                      # Lean project configuration
 ├── lean-toolchain                     # Lean version specification
-├── src/
-│   ├── Sillari_refutation.lean       # Modal logic counterexamples
-│   ├── Cubitt_Sugden_baseline.lean   # Syntactic reconstruction
-│   └── Vromen_justification_logic.lean # Justification logic solution
+├── Sillari_refutation.lean            # Modal logic counterexamples
+├── Cubitt_Sugden_baseline.lean        # Syntactic reconstruction
+├── Vromen_justification_logic.lean    # Justification logic solution
 ├── pdfs/
-│   ├── sillari_refutation.pdf        # PDF version of the Lean file
-│   ├── cubitt_sugden_baseline.pdf    # PDF version of the Lean file
+│   ├── sillari_refutation.pdf         # PDF version of the Lean file
+│   ├── cubitt_sugden_baseline.pdf     # PDF version of the Lean file
 │   ├── vromen_justification_logic.pdf # PDF version of the Lean file
 │   └── Vromen_-_2024_-_Reasoning_with_reasons_Lewis_on_common_knowledge.pdf
 └── docs/
diff --git a/lakefile.lean.backup b/lakefile.lean.backup
@@ -0,0 +1,10 @@
+import Lake
+open Lake DSL
+
+package Lewis
+
+require mathlib from git
+  "file:///Users/huubvromen/nextcloud/Leanprojects/SharedMathlib/mathlib4"
+
+@[default_target]
+lean_lib Lewis
