Define injection from rationals into reals

HOL-Theorem-Prover · Jan 25, 2024 · 5e7dda5 · 5e7dda5
1 parent d3f180d
commit 5e7dda5
Show file tree

Hide file tree

Showing 2 changed files with 398 additions and 1 deletion.
diff --git a/src/real/Holmakefile b/src/real/Holmakefile
@@ -1,5 +1,5 @@
 INCLUDES = ../integer ../hol88 ../pred_set/src/more_theories \
-           ../res_quan/src
+           ../res_quan/src ../rational
 
 TARGETS = $(subst prove_real_assumsTheory.uo,,$(DEFAULT_TARGETS))