aboutsummaryrefslogtreecommitdiffhomepage
path: root/phox/example.phx
diff options
context:
space:
mode:
authorGravatar Erik Martin-Dorel <erik@martin-dorel.org>2018-08-22 23:29:35 +0200
committerGravatar GitHub <noreply@github.com>2018-08-22 23:29:35 +0200
commit26b3bf9f070e9aee45c6e3d19bca475d4ae8ed37 (patch)
tree64b5b138c91b75c464e66eecd5dc19542ad68276 /phox/example.phx
parent3b9e1e4742a2dafce6ac2ef4bfa95d22e43c3c59 (diff)
parent7ee9486a616b12ea99490b134c1417792ef78459 (diff)
Merge pull request #200 from craff/master
Update phox support
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.
-