sci-mathematics/isabelle: Remove old

Package-Manager: portage-2.3.3

5 files changed, 0 insertions, 161 deletions

diff --git a/sci-mathematics/isabelle/files/isabelle-2012-libsha1.patch b/sci-mathematics/isabelle/files/isabelle-2012-libsha1.patch
deleted file mode 100644
index 06933669de7f..000000000000
--- a/sci-mathematics/isabelle/files/isabelle-2012-libsha1.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- Isabelle2012-orig/src/Pure/General/sha1_polyml.ML	2012-05-20 19:34:33.000000000 +1000
-+++ Isabelle2012/src/Pure/General/sha1_polyml.ML	2012-12-05 23:24:06.263793934 +1100
-@@ -18,7 +18,7 @@
-   in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
- 
- val lib_path =
--  ("$ML_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so"))
-+  ("$SHA1_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so"))
-   |> Path.explode;
- 
- fun digest_external str =
diff --git a/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch b/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch
deleted file mode 100644
index 7066c6b875a2..000000000000
--- a/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch
+++ /dev/null
@@ -1,19 +0,0 @@
---- Isabelle2013-orig/etc/settings	2013-02-13 00:31:02.000000000 +1100
-+++ Isabelle2013/etc/settings	2013-08-17 14:47:46.045988000 +1000
-@@ -176,3 +176,16 @@
- #ISABELLE_GHC="/usr/bin/ghc"
- #ISABELLE_OCAML="/usr/bin/ocaml"
- #ISABELLE_SWIPL="/usr/bin/swipl"
-+
-+# Poly/ML Gentoo (x86_64)
-+ML_PLATFORM=x86_64-linux
-+ML_HOME="/usr/bin"
-+ML_SYSTEM=polyml-5.5.0
-+ML_OPTIONS="-H 1000"
-+ML_SOURCES="/usr/src/debug/dev-lang/polyml-5.5.0"
-+
-+# Proof General home
-+PROOFGENERAL_HOME="/usr/share/emacs/site-lisp/ProofGeneral"
-+PROOFGENERAL_OPTIONS=""
-+#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"
-+
diff --git a/sci-mathematics/isabelle/files/isabelle-2013.2-HOL-Predicate_Compile_Examples.patch b/sci-mathematics/isabelle/files/isabelle-2013.2-HOL-Predicate_Compile_Examples.patch
deleted file mode 100644
index e1253016837b..000000000000
--- a/sci-mathematics/isabelle/files/isabelle-2013.2-HOL-Predicate_Compile_Examples.patch
+++ /dev/null
@@ -1,89 +0,0 @@
---- Isabelle2013-2-orig/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	2013-12-06 02:18:50.000000000 +1100
-+++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	2014-02-09 22:21:20.676081140 +1100
-@@ -87,7 +87,7 @@
- *}
- 
- lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
--quickcheck[tester = prolog, iterations = 1, expect = counterexample]
-+quickcheck[tester = prolog, iterations = 1]
- oops
- 
- section {* Manual setup to find the counterexample *}
-@@ -115,7 +115,7 @@
- 
- lemma
-   "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
--quickcheck[tester = prolog, iterations = 1, expect = counterexample]
-+quickcheck[tester = prolog, iterations = 1]
- oops
- 
- section {* Using a global limit for limiting the execution *} 
-@@ -151,7 +151,7 @@
- 
- lemma
-   "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
--quickcheck[tester = prolog, iterations = 1, expect = counterexample]
-+quickcheck[tester = prolog, iterations = 1]
- oops
- 
- end
-\ No newline at end of file
---- Isabelle2013-2-orig/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	2013-12-06 02:18:50.000000000 +1100
-+++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	2014-02-09 22:27:26.826238011 +1100
-@@ -36,7 +36,7 @@
- 
- lemma
-   "S\<^sub>1p w \<Longrightarrow> w = []"
--quickcheck[tester = prolog, iterations=1, expect = counterexample]
-+quickcheck[tester = prolog, iterations=1]
- oops
- 
- definition "filter_a = filter (\<lambda>x. x = a)"
-@@ -70,7 +70,7 @@
- 
- theorem S\<^sub>1_sound:
- "S\<^sub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
--quickcheck[tester = prolog, iterations=1, expect = counterexample]
-+quickcheck[tester = prolog, iterations=1]
- oops
- 
- 
-@@ -94,7 +94,7 @@
- 
- theorem S\<^sub>2_sound:
-   "S\<^sub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
--quickcheck[tester = prolog, iterations=1, expect = counterexample]
-+quickcheck[tester = prolog, iterations=1]
- oops
- 
- inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where
-@@ -171,4 +171,4 @@
- hide_const a b
- 
- 
--end
-\ No newline at end of file
-+end
---- Isabelle2013-2-orig/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	2013-12-06 02:18:50.000000000 +1100
-+++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	2014-02-09 22:21:20.677081168 +1100
-@@ -95,7 +95,7 @@
- 
- lemma
-   "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
--quickcheck[tester = prolog, iterations = 1, expect = counterexample]
-+quickcheck[tester = prolog, iterations = 1]
- oops
- 
- text {* Verifying that the found counterexample really is one by means of a proof *}
---- Isabelle2013-2-orig/src/HOL/Predicate_Compile_Examples/List_Examples.thy	2013-12-06 02:18:50.000000000 +1100
-+++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/List_Examples.thy	2014-02-09 22:21:20.678081196 +1100
-@@ -24,7 +24,7 @@
- lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
- quickcheck[tester = random, iterations = 10000]
- quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
--quickcheck[tester = prolog, expect = counterexample]
-+quickcheck[tester = prolog]
- oops
- 
- end
-\ No newline at end of file
diff --git a/sci-mathematics/isabelle/files/isabelle-2015-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2015-classpath.patch
deleted file mode 100644
index 3783e46cb707..000000000000
--- a/sci-mathematics/isabelle/files/isabelle-2015-classpath.patch
+++ /dev/null
@@ -1,26 +0,0 @@
---- Isabelle2015-orig/lib/Tools/java	2015-05-25 20:06:24.000000000 +1000
-+++ Isabelle2015/lib/Tools/java	2015-07-07 16:00:19.283326554 +1000
-@@ -10,5 +10,5 @@
- unset CLASSPATH
- 
- isabelle_java java "${JAVA_ARGS[@]}" \
--  -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
-+  -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11)")" "$@"
- 
---- Isabelle2015-orig/lib/Tools/scala	2015-05-25 20:06:24.000000000 +1000
-+++ Isabelle2015/lib/Tools/scala	2015-07-07 16:00:45.926327297 +1000
-@@ -14,4 +14,4 @@
- done
- 
- isabelle_scala scala "${SCALA_ARGS[@]}" \
--  -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
-+  -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11)")" "$@"
---- Isabelle2015-orig/lib/Tools/scalac	2015-05-25 20:06:24.000000000 +1000
-+++ Isabelle2015/lib/Tools/scalac	2015-07-07 15:59:33.906325289 +1000
-@@ -7,5 +7,5 @@
- isabelle_admin_build jars || exit $?
- 
- isabelle_scala scalac -Dfile.encoding=UTF-8 \
--  -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
-+  -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11)")" "$@"
- 
diff --git a/sci-mathematics/isabelle/files/isabelle-2015-jfreechart-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2015-jfreechart-classpath.patch
deleted file mode 100644
index 9594d28c86a2..000000000000
--- a/sci-mathematics/isabelle/files/isabelle-2015-jfreechart-classpath.patch
+++ /dev/null
@@ -1,16 +0,0 @@
---- Isabelle2015-orig/contrib/jfreechart-1.0.14-1/etc/settings	2013-09-12 07:46:57.000000000 +1000
-+++ Isabelle2015/contrib/jfreechart-1.0.14-1/etc/settings	2015-07-07 17:22:55.716464804 +1000
-@@ -1,9 +1,8 @@
- # -*- shell-script -*- :mode=shellscript:
- 
- JFREECHART_HOME="$COMPONENT"
--JFREECHART_JAR_NAMES="iText-2.1.5.jar jcommon-1.0.18.jar jfreechart-1.0.14.jar"
--
--classpath "$JFREECHART_HOME/lib/iText-2.1.5.jar"
--classpath "$JFREECHART_HOME/lib/jcommon-1.0.18.jar"
--classpath "$JFREECHART_HOME/lib/jfreechart-1.0.14.jar"
-+JFREECHART_JAR_NAMES="$(java-config --classpath itext | sed -e 's@:@ @g' -e 's@/[^ ]*/@@g') $(java-config --classpath jcommon-1.0 | sed -e 's@:@ @g' -e 's@/[^ ]*/@@g') $(java-config --classpath jfreechart-1.0 | sed -e 's@:@ @g' -e 's@/[^ ]*/@@g')"
- 
-+classpath "$(java-config --classpath itext)"
-+classpath "$(java-config --classpath jcommon-1.0)"
-+classpath "$(java-config --classpath jfreechart-1.0)"