cpet/freebsd-ports
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update to 2009.2

Browse Source 
PR:		ports/149736
Submitted by:	Timothy Beyer (maintainer)
This commit is contained in:
Max Brazhnikov 2010-10-30 18:34:26 +00:00
parent 78cbea96d3
commit 6b71027429
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=263798
10 changed files with 3343 additions and 2627 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

43
math/isabelle/Makefile
View File

@ -6,40 +6,45 @@
#
PORTNAME= isabelle
PORTVERSION= 2009
PORTREVISION= 2
PORTVERSION= 2009.2
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= Isabelle2009
DISTNAME= Isabelle2009-2
.if !defined(NOPORTDOCS)
DISTFILES= Isabelle2009.tar.gz \
Isabelle2009_library.tar.gz \
Isabelle2009_pdf.tar.gz
DISTFILES= ${DISTNAME}.tar.gz \
${DISTNAME}_library.tar.gz
.endif
MAINTAINER= beyert@cs.ucr.edu
COMMENT= A generic proof assistant
BROKEN= bad plist
LICENSE= BSD
LICENSE_FILE= ${WRKSRC}/COPYRIGHT
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= POLYML "Use Poly/ML (fast but broken) instead of SML/NJ" 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_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+= EMACS_PKG "Build with Emacs Packages" off
USE_PERL5= yes
USE_EMACS= yes # for EMACS_SITE_LISPDIR
EMACS_NO_BUILD_DEPENDS=yes
EMACS_NO_RUN_DEPENDS=yes
.if defined(WITH_EMACS_PKG)
USE_EMACS= yes # for EMACS_SITE_LISPDIR
EMACS_NO_BUILD_DEPENDS=yes
EMACS_NO_RUN_DEPENDS=yes
RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral
.else
.endif
BUILD_DEPENDS+= bash:${PORTSDIR}/shells/bash
RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral
RUN_DEPENDS+= bash:${PORTSDIR}/shells/bash
DOCFILES= Contents *.pdf *.eps *.ps *.dvi
@ -95,12 +100,12 @@ EXTRA_HOL+=-m HOL4
HEAP_HOL_HOL4="@comment "
.endif
.if defined(WITH_SMLNJ)
.if !defined(WITH_POLYML)
ML_SYSTEM= smlnj-110
ML_HOME= ${LOCALBASE}/bin
ML_OPTIONS= @SMLdebug=/dev/null
ML_HOME= ${LOCALBASE}/smlnj/bin
ML_OPTIONS= -Ccontrol.poly-eq-warn=false @SMLdebug=/dev/null
.else
ML_SYSTEM= polyml-5.2
ML_SYSTEM= polyml-5.3
ML_HOME= ${LOCALBASE}/bin
ML_OPTIONS= -H 500
ML_DBASE= ""
@ -114,7 +119,7 @@ PLIST_SUB+= HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM} \
HEAP_HOL_WORD=${HEAP_HOL_WORD} \
HEAP_HOL_TLA=${HEAP_HOL_TLA} \
HEAP_HOL_HOL4=${HEAP_HOL_HOL4}
.if defined(WITH_SMLNJ)
.if !defined(WITH_POLYML)
BUILD_DEPENDS+= smlnj-devel>=110.71:${PORTSDIR}/lang/sml-nj-devel
MAKE_ENV+= SMLNJ_DEVEL=yes
.else

13
math/isabelle/distinfo
View File

@ -1,9 +1,4 @@
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
SHA256 (Isabelle2009-2.tar.gz) = f92a275b78bd8844de47a5902e339b58f3b768c07a7fb19d8e606b68499d5ac4
SIZE (Isabelle2009-2.tar.gz) = 25193255
SHA256 (Isabelle2009-2_library.tar.gz) = 1cf4cc438185146367938308e01be2f29b793d6c343299aa697def9a098e63aa
SIZE (Isabelle2009-2_library.tar.gz) = 54438382

115
math/isabelle/files/patch-etc-settings
View File

@ -1,16 +1,12 @@
--- 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!)
###
--- etc/settings.orig 2010-06-21 02:24:19.000000000 -0700
+++ etc/settings 2010-08-16 14:53:16.000000000 -0700
@@ -15,19 +15,7 @@
# not invent new ML system names unless you know what you are doing.
# Only one of the sections below should be activated.
-# 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/ML 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")
-ML_PLATFORM="$ISABELLE_PLATFORM"
-ML_HOME=$(choosefrom \
- "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
- "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
@ -20,48 +16,26 @@
- $POLY_HOME)
-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
-ML_OPTIONS="-H 200"
-ML_DBASE=""
-
-# Poly/ML 5.1
-#ML_PLATFORM=x86-linux
-#ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-5.1
-#ML_OPTIONS="-H 500"
-
-# Poly/ML 5.1 (64 bit)
-#ML_PLATFORM=x86_64-linux
-#ML_HOME=/usr/local/polyml/x86_64-linux
-#ML_SYSTEM=polyml-5.1
-#ML_OPTIONS="-H 1000"
-
-# Poly/ML 4.2.0
-#ML_PLATFORM=x86-linux
-#ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-4.2.0
-#ML_OPTIONS="-H 80"
-
-# Standard ML of New Jersey (slow!)
-#ML_SYSTEM=smlnj-110
-#ML_HOME="/usr/local/smlnj/bin"
-#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_SOURCES="$ML_HOME/../src"
+
# Poly/ML 5.3.0
#ML_PLATFORM=x86-linux
@@ -50,6 +38,13 @@
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
#SMLNJ_CYGWIN_RUNTIME=1
+# FreeBSD PolyML Settings
+ML_SYSTEM=%%ML_SYSTEM%%
+ML_HOME=%%ML_HOME%%
+ML_OPTIONS=%%ML_OPTIONS%%
+ML_PLATFORM=%%ML_PLATFORM%%
+ML_DBASE=%%ML_DBASE%%
+
###
### JVM components (Scala or Java)
@@ -81,7 +37,7 @@
@@ -64,7 +59,7 @@
### Interactive sessions (cf. isabelle tty)
###
@ -70,7 +44,7 @@
[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
@@ -131,7 +87,7 @@
@@ -109,7 +104,7 @@
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
# Location for temporary files (should be on a local file system).
@ -79,7 +53,7 @@
# 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 @@
@@ -136,7 +131,7 @@
###
# Where to look for docs (multiple dirs separated by ':').
@ -88,7 +62,7 @@
# Preferred document format
ISABELLE_DOC_FORMAT=pdf
@@ -191,9 +147,7 @@
@@ -173,9 +168,7 @@
PROOFGENERAL_HOME=$(choosefrom \
"$ISABELLE_HOME/contrib/ProofGeneral" \
"$ISABELLE_HOME/../ProofGeneral" \
@ -99,39 +73,20 @@
"")
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" \
"")
@@ -201,9 +194,9 @@
## Set HOME only for tools you have installed!
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" \
"")
# External provers
-#E_HOME=/usr/local/bin
-#SPASS_HOME=/usr/local/bin
-#VAMPIRE_HOME=/usr/local/bin
+#E_HOME=%%PREFIX%%/bin
+#SPASS_HOME=%%PREFIX%%/bin
+#VAMPIRE_HOME=%%PREFIX%%/bin
# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
@@ -253,24 +205,24 @@
#HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
@@ -214,24 +207,24 @@
#SVC_MACHINE=sparc-sun-solaris
# Mucke (mu-calculus model checker)
@ -160,5 +115,5 @@
-#JERUSAT_HOME=/usr/local/bin
+#JERUSAT_HOME=%%PREFIX%%/bin
# For configuring HOL/Matrix/cplex
# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
# CSDP (SDP Solver, cf. Isabelle/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML)
#CSDP_EXE=csdp

25
math/isabelle/files/patch-lib-scripts-run_smlnj
View File

@ -1,25 +0,0 @@
--- 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
+export SMLNJ_DEVEL=yes
SML="$ML_HOME/sml"
-ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
check_mlhome_file "$SML"
-check_mlhome_file "$ARCH_N_OPSYS"
@@ -83,8 +82,7 @@
## fix heap file name and permissions
if [ -n "$OUTFILE" ]; then
- eval $("$ARCH_N_OPSYS")
- [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS"
+ [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ML_PLATFORM"
HEAP="$OUTFILE.$HEAP_SUFFIX"
check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \
[ -n "$NOWRITE" ] && chmod -w "$OUTFILE"

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

@ -1,15 +0,0 @@
--- 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
View File

@ -1,18 +0,0 @@
--- 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
View File

@ -1,29 +0,0 @@
--- 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
View File

@ -1,65 +0,0 @@
--- 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
View File

@ -1,83 +0,0 @@
--- 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 =

5564
math/isabelle/pkg-plist
View File

File diff suppressed because it is too large Load Diff