From af9234996fb53a4e7c0ec404d8dd275df17f1ccd Mon Sep 17 00:00:00 2001
From: mark
Date: Thu, 16 Feb 2012 17:09:21 +0000
Subject: First version of HOL Light tactic recording. See INSTRUCTIONS and
 LIMITATIONS files for more details. Currently works for flattening
 "packaged-up" tactic proofs into g/e commands. Won't work for most proofs
 because most tactics/thms haven't been promoted. Support for exporting proof
 graph as a series of goal pairs. Support for displaying extra information to
 be intercepter by PG for Prooftree.

---
 hol-light/TacticRecording/examples4.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 hol-light/TacticRecording/examples4.ml

(limited to 'hol-light/TacticRecording/examples4.ml')

diff --git a/hol-light/TacticRecording/examples4.ml b/hol-light/TacticRecording/examples4.ml
new file mode 100644
index 00000000..3178f656
--- /dev/null
+++ b/hol-light/TacticRecording/examples4.ml
@@ -0,0 +1,13 @@
+pg_mode_on ();;
+get_pg_mode ();;
+
+g `(?x:num. p(x) /\ q(x) /\ r(x)) ==> (?x. r(x) /\ p(x)) /\ (?x. p(x) /\ (q(x) <=> r(x)))`;;
+e (STRIP_TAC);;
+e (STRIP_TAC);;
+e (X_META_EXISTS_TAC `n1:num` THEN CONJ_TAC);;
+e (FIRST_X_ASSUM(UNIFY_ACCEPT_TAC [`n1:num`]));;
+e (ASM_REWRITE_TAC[]);;
+e (X_META_EXISTS_TAC `n2:num` THEN CONJ_TAC);;
+e (FIRST_X_ASSUM(UNIFY_ACCEPT_TAC [`n2:num`]));;
+e (ASM_REWRITE_TAC[]);;
+let th = top_thm ();;
-- 
cgit v1.2.3