From 403aa59a2c8095b98e62fde82f116433b540064b Mon Sep 17 00:00:00 2001
From: mark <>
Date: Thu, 23 Feb 2012 11:02:46 +0000
Subject: *** empty log message ***

---
 hol-light/TacticRecording/graveyard.ml | 12 ------------
 1 file changed, 12 deletions(-)
 delete mode 100644 hol-light/TacticRecording/graveyard.ml

(limited to 'hol-light')

diff --git a/hol-light/TacticRecording/graveyard.ml b/hol-light/TacticRecording/graveyard.ml
deleted file mode 100644
index db5c733d..00000000
--- a/hol-light/TacticRecording/graveyard.ml
+++ /dev/null
@@ -1,12 +0,0 @@
-
-
-(* Utility for applying tactic and incorproating results into goal tree.      *)
-(* Takes an "infotactic", i.e. like a normal tactic that works on 'goal' and  *)
-(* returns 'goalstate', but that also returns 'finfo' which summarises the    *)
-(* operation.  These are easily formed by tagging normal tactics.             *)
-
-let infotactic_wrap0 (infotac:goal->(goalstate*finfo)) (gx:xgoal) : xgoalstate =
-  let (g,id) = dest_xgoal gx in
-  let ((meta,gs,just),gst) = infotac g in
-  let gxs = extend_gtree id gst gs in
-  (meta,gxs,just);;
-- 
cgit v1.2.3