# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1648147811 0
# Node ID 1fb80d2a778dd7483c00ce6e50540d8af4ef506e
# Parent  fb8833d2c606073f238b5468a72f5114f52b989d
really removing Dedekind_real

diff -r fb8833d2c606 -r 1fb80d2a778d src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Mar 24 18:28:51 2022 +0000
+++ b/src/HOL/ROOT	Thu Mar 24 18:50:11 2022 +0000
@@ -663,7 +663,6 @@
     Conditional_Parametricity_Examples
     Cubic_Quartic
     Datatype_Record_Examples
-    Dedekind_Real
     Erdoes_Szekeres
     Eval_Examples
     Executable_Relation