Add isabelle 2004, a generic proof assistant.

PR:		84859
Submitted by:	Timothy Bourke <timbob@bigpond.com>

1 files changed, 122 insertions, 0 deletions

diff --git a/math/isabelle/files/patch-etc-settings b/math/isabelle/files/patch-etc-settings
new file mode 100644
index 000000000000..5a16d33a34ff
--- /dev/null
+++ b/math/isabelle/files/patch-etc-settings
@@ -0,0 +1,122 @@
+--- etc/settings.orig	Tue Jun  8 10:29:49 2004
++++ etc/settings	Fri Aug 12 17:22:30 2005
+@@ -13,61 +13,12 @@
+ # binaries.  Do not invent new ML system names unless you know what
+ # you are doing.  Only one of the sections below should be activated.
+ 
+-
+-# try finding the poly packages from the Isabelle site in the usual places
+-POLYML_HOME=$(choosefrom \
+-  "$ISABELLE_HOME/contrib/polyml" \
+-  "$ISABELLE_HOME/../polyml" \
+-  "/usr/share/polyml" \
+-  "/usr/local/polyml" \
+-  "/opt/polyml")
+-
+-if [ -n "$POLYML_HOME" -a -e "$POLYML_HOME/bin/polyml-version" ]; then
+-  # looks like Isabelle poly packages
+-  ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
+-  ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
+-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+-  ML_OPTIONS="-h 15000"
+-elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
+-  # maybe a shrink-wrapped polyml on x86-linux ...
+-
+-  # Poly/ML 4.0, 4.1, 4.1.x
+-  # include version number, needed for choosing right options
+-  ML_SYSTEM=polyml-4.1.3    
+-  # processor/OS type
+-  ML_PLATFORM=x86-linux
+-  # where to find binaries
+-  ML_HOME=/usr/bin
+-  # where to find the standard database
+-  ML_DBASE=/usr/lib/poly/ML_dbase
+-  # options to pass to poly
+-  ML_OPTIONS="-h 15000"
+-fi
+-
+-# Standard ML of New Jersey 110 or later
+-#ML_SYSTEM=smlnj-110
+-#ML_HOME="$ISABELLE_HOME/../smlnj/bin"
+-#ML_OPTIONS="@SMLdebug=/dev/null"
+-#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
+-
+-# MLWorks 2.0
+-#ML_SYSTEM=mlworks
+-#ML_HOME="$ISABELLE_HOME/../mlworks/bin"
+-#ML_OPTIONS=""
+-#ML_PLATFORM=""
+-
+-# Moscow ML 2.00 or later (experimental!)
+-#ML_SYSTEM=mosml
+-#ML_HOME="$ISABELLE_HOME/../mosml/bin"
+-#ML_PLATFORM=""
+-#ML_OPTIONS=""
+-
+-# Standard ML of New Jersey 0.93
+-#ML_SYSTEM=smlnj-0.93
+-#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
+-#ML_OPTIONS=""
+-#ML_PLATFORM=""
+-
++# %%ML_COMMENT%%
++ML_SYSTEM=%%ML_SYSTEM%%
++ML_HOME=%%ML_HOME%%
++ML_OPTIONS=%%ML_OPTIONS%%
++ML_PLATFORM=x86-bsd
++ML_DBASE=%%ML_DBASE%%
+ 
+ ###
+ ### Compilation options for isatool usedir
+@@ -79,7 +30,6 @@
+ # for overriding proof objects in HOL image
+ HOL_PROOF_OBJECTS=""
+ 
+-
+ ###
+ ### Document preparation
+ ###
+@@ -155,7 +105,7 @@
+ ###
+ 
+ #Where to look for docs (multiple dirs separated by ':').
+-ISABELLE_DOCS="$ISABELLE_HOME/doc"
++ISABELLE_DOCS="%%PREFIX%%/share/doc/isabelle"
+ 
+ #The dvi file viewer
+ DVI_VIEWER=xdvi
+@@ -181,12 +131,7 @@
+ 
+ # Proof General path, look in a variety of places
+ ISABELLE_INTERFACE=$(choosefrom \
+-  "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \
+-  "$ISABELLE_HOME/../ProofGeneral/isar/interface" \
+-  "/usr/share/ProofGeneral/isar/interface" \
+-  "/usr/local/ProofGeneral/isar/interface" \
+-  "/opt/ProofGeneral/isar/interface" \
+-  "/usr/share/emacs/ProofGeneral/isar/interface" \
++  "%%PREFIX%%/bin/proofgeneral" \
+   "$ISABELLE_INTERFACE")
+ 
+ # Options to pass to Isabelle command when PG is selected as interface
+@@ -196,20 +141,9 @@
+ # try xemacs first, else emacs
+ type -path xemacs >/dev/null || PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS"
+ 
+-
+-# X-Symbol installation location (for Proof General, obsolete for PG >= 3.5)
+-XSYMBOL_HOME=$(choosefrom \
+-  "$ISABELLE_HOME/contrib/x-symbol" \
+-  "$ISABELLE_HOME/../x-symbol" \
+-  "/usr/share/x-symbol" \
+-  "/usr/local/x-symbol" \
+-  "/opt/x-symbol" \
+-  "")
+-
+ # Executed before xemacs with ProofGeneral is called.
+ # Required for remote fonts only.
+ #XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
+-
+ 
+ ###
+ ### External reasoning tools