aboutsummaryrefslogtreecommitdiffhomepage
path: root/phox/example.phx
diff options
context:
space:
mode:
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.
+