mykola/freebsd-ports
1
0
Fork 0
forked from Lainports/freebsd-ports
Code Pull requests Activity

- Update to 2009

Browse source 
PR:		139737
Submitted by:	Timothy Bourke <timbob@bigpond.com> (maintainer)
This commit is contained in:
Martin Wilke 2009-10-29 22:23:28 +00:00
parent a850fae434
commit f8625babef
10 changed files with 1642 additions and 671 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

91
math/isabelle/Makefile
View file

@ -6,16 +6,16 @@
#
PORTNAME= isabelle
PORTVERSION= 2008
PORTVERSION= 2009
CATEGORIES= math
MASTER_SITES= http://isabelle.in.tum.de/dist/ \
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ \
http://mirror.cse.unsw.edu.au/pub/isabelle/dist/
DISTNAME= Isabelle2008
DISTNAME= Isabelle2009
.if !defined(NOPORTDOCS)
DISTFILES= Isabelle2008.tar.gz \
Isabelle2008_library.tar.gz \
Isabelle2008_pdf.tar.gz
DISTFILES= Isabelle2009.tar.gz \
Isabelle2009_library.tar.gz \
Isabelle2009_pdf.tar.gz
.endif
MAINTAINER= timbob@bigpond.com
@ -25,15 +25,16 @@ OPTIONS= SMLNJ "Use SML/NJ (devel) instead of faster Poly/ML" off
OPTIONS+= RLWRAP "Use rlwrap as line editor" on
OPTIONS+= LEDIT "Use ledit as line editor" off
OPTIONS+= HOL_ALGEBRA "Build optional heap: HOL-Algebra" off
OPTIONS+= HOL_COMPLEX "Build optional heap: HOL-Complex" off
OPTIONS+= HOL_MATRIX "Build optional heap: HOL-Complex-Matrix" off
OPTIONS+= HOL_NOMINAL "Build optional heap: HOL-Nominal" off
OPTIONS+= HOL_NSA "Build optional heap: HOL-NSA" off
OPTIONS+= HOL_WORD "Build optional heap: HOL-Word" off
OPTIONS+= HOL_TLA "Build optional heap: TLA" off
OPTIONS+= HOL_HOL4 "Build optional heap: HOL4" off
OPTIONS+= HOLCF_IOA "Build optional heap: IOA" off
USE_PERL5= yes
USE_EMACS= yes # for EMACS_SITE_LISPDIR
EMACS_NO_BUILD_DEPENDS=yes
EMACS_NO_RUN_DEPENDS=yes
BUILD_DEPENDS+= bash:${PORTSDIR}/shells/bash
RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral
RUN_DEPENDS+= bash:${PORTSDIR}/shells/bash
@ -56,44 +57,40 @@ LINE_EDIT= ""
.if defined(WITH_HOL_ALGEBRA)
HEAP_HOL_ALGEBRA=""
EXTRA_HOL+=-m HOL-Algebra
.else
HEAP_HOL_ALGEBRA="@comment "
.endif
.if defined(WITH_HOL_COMPLEX)
HEAP_HOL_COMPLEX=""
.else
HEAP_HOL_COMPLEX="@comment "
.endif
.if defined(WITH_HOL_MATRIX)
HEAP_HOL_COMPLEX_MATRIX=""
.else
HEAP_HOL_COMPLEX_MATRIX="@comment "
.endif
.if defined(WITH_HOL_NOMINAL)
HEAP_HOL_NOMINAL=""
EXTRA_HOL+=-m HOL-Nominal
.else
HEAP_HOL_NOMINAL="@comment "
.endif
.if defined(WITH_HOL_NSA)
HEAP_HOL_NSA=""
EXTRA_HOL+=-m HOL-NSA
.else
HEAP_HOL_NSA="@comment "
.endif
.if defined(WITH_HOL_WORD)
HEAP_HOL_WORD=""
EXTRA_HOL+=-m HOL-Word
.else
HEAP_HOL_WORD="@comment "
.endif
.if defined(WITH_HOL_TLA)
HEAP_HOL_TLA=""
EXTRA_HOL+=-m TLA
.else
HEAP_HOL_TLA="@comment "
.endif
.if defined(WITH_HOL_HOL4)
HEAP_HOL_HOL4=""
EXTRA_HOL+=-m HOL4
.else
HEAP_HOL_HOL4="@comment "
.endif
.if defined(WITH_HOLCF_IOA)
HEAP_HOLCF_IOA=""
.else
HEAP_HOLCF_IOA="@comment "
.endif
.if defined(WITH_SMLNJ)
ML_SYSTEM= smlnj-110
@ -107,21 +104,19 @@ ML_DBASE= ""
.endif
ML_PLATFORM= x86-bsd
PLIST_SUB= HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM} \
PLIST_SUB+= HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM} \
HEAP_HOL_ALGEBRA=${HEAP_HOL_ALGEBRA} \
HEAP_HOL_COMPLEX=${HEAP_HOL_COMPLEX} \
HEAP_HOL_COMPLEX_MATRIX=${HEAP_HOL_COMPLEX_MATRIX} \
HEAP_HOL_NOMINAL=${HEAP_HOL_NOMINAL} \
HEAP_HOL_NSA=${HEAP_HOL_NSA} \
HEAP_HOL_WORD=${HEAP_HOL_WORD} \
HEAP_HOL_TLA=${HEAP_HOL_TLA} \
HEAP_HOL_HOL4=${HEAP_HOL_HOL4} \
HEAP_HOLCF_IOA=${HEAP_HOLCF_IOA}
HEAP_HOL_HOL4=${HEAP_HOL_HOL4}
.if defined(WITH_SMLNJ)
BUILD_DEPENDS+= smlnj-devel>=110.65:${PORTSDIR}/lang/sml-nj-devel
BUILD_DEPENDS+= smlnj-devel>=110.71:${PORTSDIR}/lang/sml-nj-devel
MAKE_ENV+= SMLNJ_DEVEL=yes
.else
BUILD_DEPENDS+= polyml>=5.2:${PORTSDIR}/lang/polyml
RUN_DEPENDS+= polyml>=5.2:${PORTSDIR}/lang/polyml
BUILD_DEPENDS+= polyml>=5.2.1:${PORTSDIR}/lang/polyml
RUN_DEPENDS+= polyml>=5.2.1:${PORTSDIR}/lang/polyml
.endif
NO_INSTALL_MANPAGES=yes
@ -137,7 +132,10 @@ post-patch:
s|%%ML_DBASE%%|${ML_DBASE}|; \
s|%%ML_PLATFORM%%|${ML_PLATFORM}|; \
s|%%PREFIX%%|${PREFIX}|; \
s|%%LINE_EDIT%%|${LINE_EDIT}|" \
s|%%LINE_EDIT%%|${LINE_EDIT}|; \
s|%%SYSTMPDIR%%|/tmp|; \
s|%%JAVASHAREDIR%%|${PREFIX}/share/java|; \
s|%%EMACS_SITE_LISPDIR%%|${EMACS_SITE_LISPDIR}|" \
${WRKSRC}/etc/settings.presed > ${WRKSRC}/etc/settings
@${RM} ${WRKSRC}/etc/settings.presed
@${TOUCH} ${WRKSRC}/contrib/.keep
@ -145,33 +143,14 @@ post-patch:
${WRKSRC}/lib/scripts/run-smlnj
post-build:
.if defined(WITH_HOL_ALGEBRA)
${WRKSRC}/build -b -m HOL-Algebra HOL
.endif
.if defined(WITH_HOL_COMPLEX)
${WRKSRC}/build -b -m HOL-Complex HOL
.endif
.if defined(WITH_HOL_MATRIX)
${WRKSRC}/build -b -m HOL-Complex-Matrix HOL
.endif
.if defined(WITH_HOL_NOMINAL)
${WRKSRC}/build -b -m HOL-Nominal HOL
.endif
.if defined(WITH_HOL_WORD)
${WRKSRC}/build -b -m HOL-Word HOL
.endif
.if defined(WITH_HOL_TLA)
${WRKSRC}/build -b -m TLA HOL
.endif
.if defined(WITH_HOL_HOL4)
${WRKSRC}/build -b -m HOL4 HOL
.endif
.if defined(WITH_HOLCF_IOA)
${WRKSRC}/build -b -m IOA HOLCF
.if defined(EXTRA_HOL)
${WRKSRC}/build -b ${EXTRA_HOL} HOL
.endif
post-install:
${WRKSRC}/bin/isatool ${INSTALL} -d ${PREFIX}/share/isabelle -p ${PREFIX}/bin
${WRKSRC}/bin/isabelle install \
-d ${PREFIX}/share/isabelle \
-p ${PREFIX}/bin
.if !defined(NOPORTDOCS)
${MKDIR} ${DOCSDIR}
.for file in ${DOCFILES}

18
math/isabelle/distinfo
View file

@ -1,9 +1,9 @@
MD5 (Isabelle2008.tar.gz) = 4ebd3288458b6a87979b211bf8fe3e15
SHA256 (Isabelle2008.tar.gz) = 27c963524992d88af57184a19ede96325bd8c117bd29d86664d25183dfffc140
SIZE (Isabelle2008.tar.gz) = 7932744
MD5 (Isabelle2008_library.tar.gz) = feff661e1b5e7279f3dedb9924e03973
SHA256 (Isabelle2008_library.tar.gz) = a5b6d8d22b004b14e94ef8fa16de272b669888a4847f512dbb7874b531612aba
SIZE (Isabelle2008_library.tar.gz) = 37598185
MD5 (Isabelle2008_pdf.tar.gz) = e52b6f445b06a4a0b7c90d703196c37d
SHA256 (Isabelle2008_pdf.tar.gz) = 71b98cb7ae0e5a2d9645e16d2f1f274cc5626ffade96d248ac48529329c79bf7
SIZE (Isabelle2008_pdf.tar.gz) = 5214045
MD5 (Isabelle2009.tar.gz) = 2b7a8d49bfba64aac7227d692c15c27b
SHA256 (Isabelle2009.tar.gz) = 49f8708962a89102cd25d9b5b7bf1298017c0689f9ced7741c124351b58f8e71
SIZE (Isabelle2009.tar.gz) = 9073615
MD5 (Isabelle2009_library.tar.gz) = 8ffcb7a25a4d110dd9060d7fbb582fc6
SHA256 (Isabelle2009_library.tar.gz) = db605638e4c66ed74069a4370cb6be776901e6ada6dfdd5104536379dbd0beef
SIZE (Isabelle2009_library.tar.gz) = 44856488
MD5 (Isabelle2009_pdf.tar.gz) = 3e964988a4cb70d1589a8c89f1e3eac7
SHA256 (Isabelle2009_pdf.tar.gz) = 0e451cabf1ece51cd989531dce14136b62c4138ace9bc618a1bd71d1c984ed70
SIZE (Isabelle2009_pdf.tar.gz) = 5757069

120
math/isabelle/files/patch-etc-settings
View file

@ -1,9 +1,13 @@
--- etc/settings.orig 2008-07-28 15:10:38.000000000 +1000
+++ etc/settings 2008-07-28 15:22:08.000000000 +1000
@@ -16,70 +16,36 @@
# not invent new ML system names unless you know what you are doing.
# Only one of the sections below should be activated.
--- etc/settings.orig 2009-10-09 10:34:33.000000000 +1100
+++ etc/settings 2009-10-09 10:37:10.000000000 +1100
@@ -11,55 +11,11 @@
### ML compiler settings (ESSENTIAL!)
###
-# ML_HOME specifies the location of the actual compiler binaries. Do
-# not invent new ML system names unless you know what you are doing.
-# Only one of the sections below should be activated.
-
-# Poly/ML 4.x/5.x (automated settings)
-POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
-ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
@ -42,37 +46,23 @@
-#ML_OPTIONS="@SMLdebug=/dev/null"
-#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-#SMLNJ_CYGWIN_RUNTIME=1
-
-# Moscow ML 2.00 (experimental!)
-#ML_SYSTEM=mosml
-#ML_HOME="/usr/local/mosml/bin"
-#ML_OPTIONS=""
-#ML_PLATFORM=""
-
+ML_SYSTEM=%%ML_SYSTEM%%
+ML_HOME=%%ML_HOME%%
+ML_OPTIONS=%%ML_OPTIONS%%
+ML_PLATFORM=%%ML_PLATFORM%%
+ML_DBASE=%%ML_DBASE%%
# Moscow ML 2.00 (experimental!)
#ML_SYSTEM=mosml
-#ML_HOME="/usr/local/mosml/bin"
+#ML_HOME="%%PREFIX%%/bin"
#ML_OPTIONS=""
#ML_PLATFORM=""
# Alice 1.4 (experimental!)
#ML_SYSTEM=alice
-#ML_HOME="/usr/local/alice/bin"
+#ML_HOME="%%PREFIX%%/bin"
#ML_OPTIONS=""
#ML_PLATFORM=""
# Poplog/PML version 15.6/2.1 (experimental!)
#ML_SYSTEM=poplogml
-#ML_HOME="/usr/local/poplog/current-poplog/bin"
+#ML_HOME="%%PREFIX%%/bin"
#ML_OPTIONS="-noinit"
#ML_SUFFIX=".psv"
#ML_PLATFORM=""
-
###
### Interactive sessions (cf. isatool tty)
### JVM components (Scala or Java)
@@ -81,7 +37,7 @@
### Interactive sessions (cf. isabelle tty)
###
-ISABELLE_LINE_EDITOR=""
@ -80,7 +70,16 @@
[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
@@ -154,7 +120,7 @@
@@ -131,7 +87,7 @@
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+ISABELLE_TMP_PREFIX="%%SYSTMPDIR%%/isabelle-$USER"
# Heap input locations. ML system identifier is included in lookup.
ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps"
@@ -157,7 +113,7 @@
###
# Where to look for docs (multiple dirs separated by ':').
@ -89,29 +88,50 @@
# Preferred document format
ISABELLE_DOC_FORMAT=pdf
@@ -189,6 +155,8 @@
@@ -191,9 +147,7 @@
PROOFGENERAL_HOME=$(choosefrom \
"$ISABELLE_HOME/contrib/ProofGeneral" \
"$ISABELLE_HOME/../ProofGeneral" \
- "/usr/local/ProofGeneral" \
- "/usr/share/ProofGeneral" \
- "/opt/ProofGeneral" \
+ "%%PREFIX%%/%%EMACS_SITE_LISPDIR%%/ProofGeneral" \
"")
# Proof General path, look in a variety of places
ISABELLE_INTERFACE=$(choosefrom \
+ "%%PREFIX%%/lib/xemacs/site-lisp/ProofGeneral/isar/interface" \
+ "%%PREFIX%%/bin/proofgeneral" \
"$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \
"$ISABELLE_HOME/../ProofGeneral/isar/interface" \
"/usr/local/ProofGeneral/isar/interface" \
@@ -211,9 +179,9 @@
## Set HOME only for tools you have installed!
PROOFGENERAL_OPTIONS=""
@@ -211,9 +165,7 @@
JEDIT_HOME=$(choosefrom \
"$ISABELLE_HOME/contrib/jedit" \
"$ISABELLE_HOME/../jedit" \
- "/usr/local/jedit" \
- "/usr/share/jedit" \
- "/opt/jedit" \
+ "%%JAVASHAREDIR%%/jedit" \
"")
# External provers
-E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "")
-VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "")
-SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "")
+E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "%%PREFIX%%/E" "")
+VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "%%PREFIX%%/Vampire" "")
+SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "%%PREFIX%%/SPASS" "")
JEDIT_JAVA_OPTIONS=""
@@ -231,17 +183,17 @@
E_HOME=$(choosefrom \
"$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \
"$ISABELLE_HOME/../E/$ML_PLATFORM" \
- "/usr/local/E" \
+ "%%PREFIX%%/E" \
"")
VAMPIRE_HOME=$(choosefrom \
"$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
"$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
- "/usr/local/Vampire" \
+ "%%PREFIX%%/Vampire" \
"")
SPASS_HOME=$(choosefrom \
"$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \
"$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \
- "/usr/local/SPASS" \
+ "%%PREFIX%%/SPASS" \
"")
# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
#HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
@@ -224,26 +192,26 @@
@@ -253,24 +205,24 @@
#SVC_MACHINE=sparc-sun-solaris
# Mucke (mu-calculus model checker)
@ -129,8 +149,6 @@
# zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
-#ZCHAFF_HOME=/usr/local/bin
+#ZCHAFF_HOME=%%PREFIX%%/bin
#ZCHAFF_VERSION=2004.5.13
#ZCHAFF_VERSION=2004.11.15
# BerkMin561 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
-#BERKMIN_HOME=/usr/local/bin

8
math/isabelle/files/patch-lib-scripts-run_smlnj
View file

@ -1,6 +1,6 @@
--- lib/scripts/run-smlnj.orig 2004-06-21 18:25:58.000000000 +1000
+++ lib/scripts/run-smlnj 2008-07-29 15:49:30.000000000 +1000
@@ -39,11 +39,10 @@
--- lib/scripts/run-smlnj.orig 2009-10-08 20:50:08.000000000 +1100
+++ lib/scripts/run-smlnj 2009-10-08 20:51:07.000000000 +1100
@@ -38,11 +38,10 @@
## compiler binaries
@ -13,7 +13,7 @@
@@ -84,8 +83,7 @@
@@ -83,8 +82,7 @@
## fix heap file name and permissions
if [ -n "$OUTFILE" ]; then

15
math/isabelle/files/patch-src-HOL-Tools-atp_manager.ML Normal file
View file

@ -0,0 +1,15 @@
--- src/HOL/Tools/atp_manager.ML.orig 2009-10-18 10:37:58.000000000 +1100
+++ src/HOL/Tools/atp_manager.ML 2009-10-18 10:39:46.000000000 +1100
@@ -77,9 +77,9 @@
fun ord ((a, _), (b, _)) = Time.compare (a, b);
);
-val lookup_thread = AList.lookup Thread.equal;
-val delete_thread = AList.delete Thread.equal;
-val update_thread = AList.update Thread.equal;
+fun lookup_thread x = AList.lookup Thread.equal x;
+fun delete_thread x = AList.delete Thread.equal x;
+fun update_thread x = AList.update Thread.equal x;
(* state of thread manager *)

18
math/isabelle/files/patch-src-HOL-Tools-atp_wrapper.ML Normal file
View file

@ -0,0 +1,18 @@
--- src/HOL/Tools/atp_wrapper.ML.orig 2009-10-18 11:13:04.000000000 +1100
+++ src/HOL/Tools/atp_wrapper.ML 2009-10-18 11:14:20.000000000 +1100
@@ -112,13 +112,13 @@
fun tptp_prover_opts max_new theory_const =
tptp_prover_opts_full max_new theory_const false;
-val tptp_prover = tptp_prover_opts 60 true;
+fun tptp_prover x = tptp_prover_opts 60 true x;
(*for structured proofs: prover must support TSTP*)
fun full_prover_opts max_new theory_const =
tptp_prover_opts_full max_new theory_const true;
-val full_prover = full_prover_opts 60 true;
+fun full_prover x = full_prover_opts 60 true x;
(* Vampire *)

29
math/isabelle/files/patch-src-HOL-Tools-int_arith.ML Normal file
View file

@ -0,0 +1,29 @@
--- src/HOL/Tools/int_arith.ML.orig 2009-04-17 01:29:56.000000000 +1000
+++ src/HOL/Tools/int_arith.ML 2009-10-17 19:35:35.000000000 +1100
@@ -229,7 +229,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val find_first_coeff = find_first_coeff []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -308,7 +308,7 @@
val dest_coeff = dest_coeff 1
val left_distrib = @{thm combine_common_factor} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -334,7 +334,7 @@
val dest_coeff = dest_fcoeff 1
val left_distrib = @{thm combine_common_factor} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
fun norm_tac ss =

65
math/isabelle/files/patch-src-HOL-Tools-int_factor_simprocs.ML Normal file
View file

@ -0,0 +1,65 @@
--- src/HOL/Tools/int_factor_simprocs.ML.orig 2009-10-17 19:46:40.000000000 +1100
+++ src/HOL/Tools/int_factor_simprocs.ML 2009-10-17 20:06:01.000000000 +1100
@@ -29,7 +29,7 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
@@ -249,7 +249,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first_t []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
@@ -261,7 +261,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
- val simp_conv = K (K (SOME @{thm mult_cancel_left}))
+ fun simp_conv _ _ = SOME @{thm mult_cancel_left}
);
(*for ordered rings*)
@@ -290,7 +290,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
- val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if}))
+ fun simp_conv _ _ = SOME @{thm zdiv_zmult_zmult1_if}
);
structure IntModCancelFactor = ExtractCommonTermFun
@@ -298,7 +298,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod}
val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
- val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1}))
+ fun simp_conv _ _ = SOME @{thm zmod_zmult_zmult1}
);
structure IntDvdCancelFactor = ExtractCommonTermFun
@@ -306,7 +306,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
- val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
+ fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
);
(*Version for all fields, including unordered ones (type complex).*)
@@ -315,7 +315,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
- val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
+ fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
);
val cancel_factors =

83
math/isabelle/files/patch-src-HOL-Tools-nat_simprocs.ML Normal file
View file

@ -0,0 +1,83 @@
--- src/HOL/Tools/nat_simprocs.ML.orig 2009-10-17 19:48:52.000000000 +1100
+++ src/HOL/Tools/nat_simprocs.ML 2009-10-18 09:59:34.000000000 +1100
@@ -142,7 +142,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first_coeff = find_first_coeff []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
[@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
@@ -231,7 +231,7 @@
val dest_coeff = dest_coeff
val left_distrib = @{thm left_add_mult_distrib} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
@@ -256,7 +256,7 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps
numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
@@ -362,7 +362,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first_t []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
@@ -373,7 +373,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
);
structure LessCancelFactor = ExtractCommonTermFun
@@ -381,7 +381,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
);
structure LeCancelFactor = ExtractCommonTermFun
@@ -389,7 +389,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
);
structure DivideCancelFactor = ExtractCommonTermFun
@@ -397,7 +397,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
);
structure DvdCancelFactor = ExtractCommonTermFun
@@ -405,7 +405,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
);
val cancel_factor =

1866
math/isabelle/pkg-plist
View file

File diff suppressed because it is too large Load diff