# HG changeset patch
# User wenzelm
# Date 1737236493 -3600
# Node ID f4cd3e67909655bbde28d6b19807d7d656ae75e8
# Parent  deb6cb34a37fe8dc59a926f381bfb480d2533997
clarified patches: avoid duplication;

diff -r deb6cb34a37f -r f4cd3e679096 src/HOL/Import/patches/patch1
--- a/src/HOL/Import/patches/patch1	Sat Jan 18 22:29:47 2025 +0100
+++ b/src/HOL/Import/patches/patch1	Sat Jan 18 22:41:33 2025 +0100
@@ -23,3 +23,9 @@
 +#use "update_database.ml";;
 +#use "statements.ml";;
 +exit 0;;
+--- hol-light/stage2.ml	1970-01-01 01:00:00.000000000 +0100
++++ hol-light-patched/stage2.ml	2025-01-18 11:12:11.384276293 +0100
+@@ -0,0 +1,3 @@
++#use "hol.ml";;
++stop_recording ();;
++exit 0;;
diff -r deb6cb34a37f -r f4cd3e679096 src/HOL/Import/patches/patch2
--- a/src/HOL/Import/patches/patch2	Sat Jan 18 22:29:47 2025 +0100
+++ b/src/HOL/Import/patches/patch2	Sat Jan 18 22:41:33 2025 +0100
@@ -359,16 +359,3 @@
  
  end;;
  
---- hol-light/stage1.ml	2025-01-18 11:12:11.373276465 +0100
-+++ hol-light-patched/stage1.ml	1970-01-01 01:00:00.000000000 +0100
-@@ -1,4 +0,0 @@
--#use "hol.ml";;
--#use "update_database.ml";;
--#use "statements.ml";;
--exit 0;;
---- hol-light/stage2.ml	1970-01-01 01:00:00.000000000 +0100
-+++ hol-light-patched/stage2.ml	2025-01-18 11:12:11.384276293 +0100
-@@ -0,0 +1,3 @@
-+#use "hol.ml";;
-+stop_recording ();;
-+exit 0;;