aboutsummaryrefslogtreecommitdiff
path: root/isa/ProofGeneral.ML
diff options
context:
space:
mode:
Diffstat (limited to 'isa/ProofGeneral.ML')
-rw-r--r--isa/ProofGeneral.ML4
1 files changed, 4 insertions, 0 deletions
diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 5d460198..e3d393a0 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -9,6 +9,10 @@
*)
+use "/home/da/isa-patches/thy_read.ML";
+open ThyRead;
+
+
signature PROOFGENERAL =
sig
val kill_goal : unit -> unit