diff --git a/examples/probability/legacy/Holmakefile b/examples/probability/legacy/Holmakefile index 5009f9a74d..559577c486 100644 --- 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 index 4428008897..3b0793c6a5 100644 --- 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