Minor cleanups

HOL-Theorem-Prover · Jan 22, 2024 · fc44313 · fc44313
1 parent b28345a
commit fc44313
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git a/examples/probability/legacy/Holmakefile b/examples/probability/legacy/Holmakefile
@@ -1,7 +1,6 @@
 INCLUDES = $(HOLDIR)/src/real $(HOLDIR)/src/res_quan/src $(HOLDIR)/src/real/analysis
 
-EXTRA_CLEANS = heap \
-	$(patsubst %Theory.uo,%Theory.html,$(DEFAULT_TARGETS))
+EXTRA_CLEANS = $(patsubst %Theory.uo,%Theory.html,$(DEFAULT_TARGETS))
 
 all: $(DEFAULT_TARGETS)
 

diff --git a/examples/probability/legacy/README.md b/examples/probability/legacy/README.md
@@ -2,6 +2,6 @@
 
 The following theories in this directory was in `$(HOLDIR)/src/probability`:
 
-	 real_measureScript.sml       * Finite Measure Theory (based on reals)
+     real_measureScript.sml       * Finite Measure Theory (based on reals)
      real_lebesgueScript.sml      * Lebesgue Integration based on Finite Measures
      real_probabilityScript.sml   * Probability Theory based on Finite Measures