Deleted file

3 files changed, 0 insertions, 249 deletions

diff --git a/lclam/README b/lclam/README
deleted file mode 100644
index 8b4e3f90..00000000
--- a/lclam/README
+++ /dev/null
@@ -1,14 +0,0 @@
-Lambda-CLAM Proof General
-
-Written by James Brotherston <jjb@dai.ed.ac.uk>.
-
-
-Status:			supported
-Maintainer:		James Brotherston <jjb@dai.ed.ac.uk>
-Lambda-CLAM homepage:   http://dream.dai.ed.ac.uk/software/systems/lambda-clam/
-
-========================================
-
-$Id$
-
-
diff --git a/lclam/example.lcm b/lclam/example.lcm
deleted file mode 100644
index 5b275814..00000000
--- a/lclam/example.lcm
+++ /dev/null
@@ -1,34 +0,0 @@
-/* File name:      example.lcm                            */
-/* Description:    Tutorial walkthrough from LClam manual */
-/* Author:         James Brotherston                      */
-/* Last modified:  20th August 2001                       */
-
-query_top_goal X assp.
-
-set_spypoint (induction_top normal_ind).
-set_spypoint sym_eval.
-
-silent_output on.
-
-pds_plan (induction_top normal_ind) assp.
-continue.
-continue.
-continue.
-
-add_theory_to_induction_scheme_list arithmetic.
-add_theory_to_sym_eval_list arithmetic.
-set_wave_rule_to_sym_eval.
-add_to_sym_eval_list [idty].
-set_wave_rule_to_sym_eval.
-remove_spypoint (induction_top normal_ind).
-remove_spypoint sym_eval.
-pds_plan (induction_top normal_ind) assp.
-
-step_by_step on.
-pds_plan (induction_top normal_ind) assp.
-continue.
-backtrack.
-try ind_strat.
-continue.
-plan_node (2::1::nil).
-abandon.
diff --git a/lclam/lclam.el b/lclam/lclam.el
deleted file mode 100644
index ae83e369..00000000
--- a/lclam/lclam.el
+++ /dev/null
@@ -1,201 +0,0 @@
-;; File name:      lclam.el
-;; Description:    Proof General instance for Lambda-CLAM
-;; Author:         James Brotherston <jjb@dai.ed.ac.uk>
-;; Last modified:  23 October 2001
-;;
-;; $Id$
-
-(require 'proof)            ; load generic parts
-(require 'proof-syntax)
-
-(eval-when-compile
-  (defvar lclam-toolbar-entries nil))
-
-;;
-;; =========== User settings for Lambda-CLAM ============
-;;
-
-(defcustom lclam-prog-name ; "~/lambda-clam-teyjus/bin/lclam"
-			   "lclam"
-  "*Name of program to run Lambda-CLAM"
-  :type 'file
-  :group 'lclam)
-
-(defcustom lclam-web-page
-  "http://dream.dai.ed.ac.uk/software/systems/lambda-clam/"
-  "URL of web page for Lambda-CLAM"
-  :type 'string
-  :group 'lclam-config)
-
-
-;;
-;; =========== Configuration of generic modes ============
-;;
-
-(defun lclam-config ()
-  "Configure Proof General scripting for Lambda-CLAM."
-  (setq
-   proof-terminal-char             ?\.
-   proof-script-comment-start      "/*"
-   proof-script-comment-end        "*/"
-   proof-goal-command-regexp       "^pds_plan"
-   proof-save-command-regexp       nil
-   proof-goal-with-hole-regexp     nil
-   proof-save-with-hole-regexp     nil
-   proof-non-undoables-regexp      nil
-   proof-undo-n-times-cmd          nil
-   proof-showproof-command         nil
-   proof-goal-command              "^pds_plan %s."
-   proof-save-command              nil
-   proof-kill-goal-command         nil
-   proof-assistant-home-page       lclam-web-page
-   proof-auto-multiple-files       nil
-   proof-prog-name		   lclam-prog-name
-   proof-shell-process-connection-type t
-   ))
-
-(defun lclam-shell-config ()
-  "Configure Proof General shell for Lambda-CLAM"
-  (setq
-   proof-shell-annotated-prompt-regexp "^lclam:"
-   proof-shell-cd-cmd                  nil
-   proof-shell-interrupt-regexp        nil
-   proof-shell-error-regexp            nil
-   proof-shell-start-goals-regexp      nil
-   proof-shell-end-goals-regexp        nil
-   proof-shell-proof-completed-regexp  "^Plan Succeeded"
-   proof-shell-init-cmd                nil
-   proof-shell-quit-cmd                "halt."
-   proof-shell-eager-annotation-start  nil
-    ))
-
-;;
-;; =========== Defining the derived modes ================
-;;
-
-(define-derived-mode lclam-proofscript-mode proof-mode
-  "Lambda-CLAM script" nil
-  (lclam-config)
-  (proof-config-done))
-
-(define-derived-mode lclam-shell-mode proof-shell-mode
-  "Lambda-CLAM shell" nil
-  (lclam-shell-config)
-  (proof-shell-config-done))
-
-(define-derived-mode lclam-response-mode proof-response-mode
-  "Lambda-CLAM response" nil
-  (proof-response-config-done))
-
-(define-derived-mode lclam-goals-mode proof-goals-mode
-  "Lambda-CLAM goals" nil
-  (proof-goals-config-done))
-
-;; Automatic selection of theory file or proof script mode
-;; .lcm -> proof script mode
-;; .def -> theory file mode
-
-(defun lclam-mode ()
-(interactive)
-(cond
-    ((proof-string-match "\\.def$" (buffer-file-name))
-    (thy-mode))
-    (t
-    (lclam-proofscript-mode)))
-)
-
-
-
-;;
-;; ============ Extra bits and pieces - JB ============
-;;
-
-;; Open .def files in theory mode from now on
-
-(setq auto-mode-alist
-      (cons '("\\.def$" . thy-mode) auto-mode-alist))
-
-;; Remove redundant toolbar buttons
-
-(setq lclam-toolbar-entries
-      (assq-delete-all 'state lclam-toolbar-entries))
-(setq lclam-toolbar-entries
-      (assq-delete-all 'context lclam-toolbar-entries))
-(setq lclam-toolbar-entries
-      (assq-delete-all 'undo lclam-toolbar-entries))
-(setq lclam-toolbar-entries
-      (assq-delete-all 'retract lclam-toolbar-entries))
-(setq lclam-toolbar-entries
-      (assq-delete-all 'qed lclam-toolbar-entries))
-
-;;
-;; ============ Theory file mode ==============
-;;
-
-(define-derived-mode thy-mode fundamental-mode "Lambda-CLAM theory file mode"
-  (thy-add-menus))
-
-(defvar thy-mode-map nil)
-
-(defun thy-add-menus ()
-  "Add Lambda-CLAM menu to current menu bar."
-  (require 'proof-script)
-  (easy-menu-define thy-mode-pg-menu
-		    thy-mode-map
-		    "PG Menu for Lambda-CLAM Proof General"
-		    (cons proof-general-name
-			  (append
-			   (list
-			   ;; A couple from the toolbar that make sense here
-			   ;; (also in proof-universal-keys)
-			    ["Issue command" proof-minibuffer-cmd t]
-			    ["Interrupt prover" proof-interrupt-process t])
-			   (list proof-buffer-menu)
-			   (list proof-help-menu))))
-
-  (easy-menu-define thy-mode-lclam-menu
-		    thy-mode-map
-		    "Menu for Lambda-CLAM Proof General, theory file mode."
-		    (cons "Theory"
-			  (list
-			   ["Next section" thy-goto-next-section t]
-			   ["Prev section" thy-goto-prev-section t]
-			   ["Insert template" thy-insert-template t]
-; da: commented out this, function is incomplete
-;                           ["Include definitions" match-and-assert-defs
-;                            :active (proof-locked-region-empty-p)]
-			   ["Process theory" process-thy-file
-			    :active (proof-locked-region-empty-p)]
-; da: commented out this, there's no retract function provided
-;                           ["Retract theory" isa-retract-thy-file
-;                            :active (proof-locked-region-full-p)]
-			   ["Next error" proof-next-error t]
-			   ["Switch to script" thy-find-other-file t])))
-
-  (easy-menu-add thy-mode-pg-menu thy-mode-map)
-  (easy-menu-add thy-mode-lclam-menu thy-mode-map)
-)
-
-(defun process-thy-file (file)
-  "Process the theory file FILE.  If interactive, use buffer-file-name."
-  (interactive (list buffer-file-name))
-  (save-some-buffers)
-  (update-thy-only file nil nil))
-
-(defun update-thy-only (file try wait)
-  "Process the theory file FILE."
-  ;; First make sure we're in the right directory to take care of
-  ;; relative "files" paths inside theory file.
-  (proof-cd-sync)
-  (proof-shell-invisible-command
-   (proof-format-filename
-    ;; %r parameter means relative (don't expand) path
-    (format "use_thy \"%s%%r\"." (if try "try_" ""))
-    (file-name-nondirectory file))
-   wait))
-
-;(defun match-and-assert-defs
-;  "Interactively process and assert definitions in theory file"
-;)
-
-(provide 'lclam)