From b0c6cae90829ba5b12a466716e4f3626e6cc70b5 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 8 Feb 2012 18:29:13 +0000 Subject: Duplicate proof --- hol-light/example.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'hol-light') diff --git a/hol-light/example.ml b/hol-light/example.ml index 1c65ce0b..7010fbc2 100644 --- a/hol-light/example.ml +++ b/hol-light/example.ml @@ -10,3 +10,10 @@ e CONJ_TAC;; e (ASM_SIMP_TAC[]);; e (ASM_SIMP_TAC[]);; let and_comms = top_thm();; + +g `A /\ B ==> B /\ A`;; +e DISCH_TAC;; +e CONJ_TAC;; +e (ASM_SIMP_TAC[]);; +e (ASM_SIMP_TAC[]);; +let and_comms2 = top_thm();; -- cgit v1.2.3