diff options
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();; |