From 7cc95a00fda26cbd6694075dca74b16c6c54f016 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 8 Feb 2012 14:18:27 +0000 Subject: Test examples for HOL Light --- etc/hol-light/example4.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 etc/hol-light/example4.ml (limited to 'etc/hol-light') diff --git a/etc/hol-light/example4.ml b/etc/hol-light/example4.ml new file mode 100644 index 00000000..3178f656 --- /dev/null +++ b/etc/hol-light/example4.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