diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 18:29:13 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 18:29:13 +0000 |
| commit | b0c6cae90829ba5b12a466716e4f3626e6cc70b5 (patch) | |
| tree | 61644e29ae00e9e92d80ef86cddb04274fc62823 /hol-light | |
| parent | 6836d87659da62abb68f6b461fb378fbc0c9b041 (diff) | |
Duplicate proof
Diffstat (limited to 'hol-light')
| -rw-r--r-- | hol-light/example.ml | 7 |
1 files changed, 7 insertions, 0 deletions
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();; |