aboutsummaryrefslogtreecommitdiff
path: root/phox/example.phx
diff options
context:
space:
mode:
authorChristophe Raffalli2000-12-22 14:03:10 +0000
committerChristophe Raffalli2000-12-22 14:03:10 +0000
commitb63dd74e45d33d5493906b3c8caf00d0b84d8146 (patch)
tree3f00fcdbe261dd874cce7d7309f3b94e3b2c225f /phox/example.phx
parent7fd3934a7915b9dcc7930d59c592089e1357309d (diff)
*** empty log message ***
Diffstat (limited to 'phox/example.phx')
-rw-r--r--phox/example.phx15
1 files changed, 14 insertions, 1 deletions
diff --git a/phox/example.phx b/phox/example.phx
index 36ece411..a0edbe48 100644
--- a/phox/example.phx
+++ b/phox/example.phx
@@ -4,6 +4,19 @@
$Id$
*)
+(*
+goal /\n:N (ack n N1 >= N2).
+intro 2.
+elim H.
+trivial.
+elim -1 [case] H0.
+trivial.
+trivial.
+save ack_lem7.
+*)
+
prop (* test *) (* just un test *) test /\X (X -> X).
+print $0.
trivial.
-save. \ No newline at end of file
+save.
+