aboutsummaryrefslogtreecommitdiffhomepage
path: root/phox/example.phx
diff options
context:
space:
mode:
authorGravatar Christophe Raffalli <raffalli@univ-savoie.fr>2017-09-22 00:28:27 +0200
committerGravatar Christophe Raffalli <raffalli@univ-savoie.fr>2017-09-22 00:28:27 +0200
commit06d72fb68fd9dd57632650f1a79de01317a6069f (patch)
tree5a2d0514349db94d7075966446ef240067dfcb23 /phox/example.phx
parent9083698d0bbd4438208fa72222438ae59684542d (diff)
phox is back
Diffstat (limited to 'phox/example.phx')
-rw-r--r--phox/example.phx22
1 files changed, 0 insertions, 22 deletions
diff --git a/phox/example.phx b/phox/example.phx
deleted file mode 100644
index 5dacbb20..00000000
--- a/phox/example.phx
+++ /dev/null
@@ -1,22 +0,0 @@
-(*
- Example proof script for PhoX Proof General
-
- $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.
-