diff options
| author | Christophe Raffalli | 2003-02-12 21:03:12 +0000 |
|---|---|---|
| committer | Christophe Raffalli | 2003-02-12 21:03:12 +0000 |
| commit | 694a4bc41311cfdff1b724b3e25644b7e20dbdb4 (patch) | |
| tree | fb8d1ec53dbca30a726f3fbea108772517e9b076 /phox/phox-fun.el | |
| parent | c6ebd146613e4255127c6d1c8036bc4a60a9aac6 (diff) | |
change for version 0.83 of PhoX
Diffstat (limited to 'phox/phox-fun.el')
| -rw-r--r-- | phox/phox-fun.el | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/phox/phox-fun.el b/phox/phox-fun.el index 7592a87e..d556a3c8 100644 --- a/phox/phox-fun.el +++ b/phox/phox-fun.el @@ -6,7 +6,7 @@ phox-forget-proof-command "del_proof %s.\n" phox-forget-new-elim-command "edel elim %s.\n" phox-forget-new-intro-command "edel intro %s.\n" - phox-forget-new-rewrite-command "edel rewrite %s.\n" + phox-forget-new-equation-command "edel equation %s.\n" phox-forget-close-def-command "edel closed %s.\n" ; phox-comments-regexp : a sequence of comments and white spaces phox-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*" @@ -54,6 +54,9 @@ phox-new-rewrite-regexp (concat "new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" phox-ident-regexp) + phox-new-equation-regexp (concat + "new_equation\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" + phox-ident-regexp) phox-close-def-regexp (concat "close_def" phox-comments-regexp @@ -95,6 +98,7 @@ or for optional argument TABLE." "edel" "new_elim" "new_intro" +"new_equation" "new_rewrite" "Data" "Inductive" @@ -190,9 +194,14 @@ or for optional argument TABLE." (concat (format phox-forget-new-intro-command (match-string 3 str)) ans))) - ((proof-string-match phox-new-rewrite-regexp str) + ((proof-string-match phox-new-rewrite-regexp str) ; deprecated + (setq ans + (concat (format phox-forget-new-equation-command + (match-string 3 str)) ans))) + + ((proof-string-match phox-new-equation-regexp str) (setq ans - (concat (format phox-forget-new-rewrite-command + (concat (format phox-forget-new-equation-command (match-string 3 str)) ans))) ((proof-string-match phox-close-def-regexp str) @@ -268,12 +277,12 @@ Gives the list of all axioms which have been used to prove the theorem." "Interactive function : ask for a string and send an eshow command to PhoX for it. -Shows the given extension-list. Possible extension lists are : rewrite -(the list of rewriting rules introduced by the new_rewrite command), -elim, intro, (the introduction and elimination rules introduced by the -new_elim and new_intro {-t} commands), closed (closed definitions -introduced by the close_def command) and tex (introduced by the -tex_syntax command)." +Shows the given extension-list. Possible extension lists are : equation +(the list of equations added to unification introduced by the new_equation +command), elim, intro, (the introduction and elimination rules +introduced by the new_elim and new_intro {-t} commands), closed +(closed definitions introduced by the close_def command) and tex +(introduced by the tex_syntax command)." (interactive "sextension list: ") (proof-shell-invisible-command (concat "eshow " extlist))) |