# HG changeset patch # User desharna # Date 1635932694 -3600 # Node ID d4a812e4f041f89d76e3c052af0984d90a50cf82 # Parent d4ef127b74df85dc9f7cd39763c564670b518bb9# Parent 591303cc04c2e3f93a14122bd8611c9ab53d1ba2 merged diff -r d4ef127b74df -r d4a812e4f041 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Tue Nov 02 13:51:29 2021 +0100 +++ b/Admin/components/components.sha1 Wed Nov 03 10:44:54 2021 +0100 @@ -195,6 +195,7 @@ 33dd96cd83f2c6a26c035b7a0ee57624655224c5 jedit-20210724.tar.gz 0e4fd4d66388ddc760fa5fbd8d4a9a3b77cf59c7 jedit-20210802.tar.gz 258d527819583d740a3aa52dfef630eed389f8c6 jedit-20211019.tar.gz +f4f3fcbd54488297a5d2fcd23a2595912d5ba80b jedit-20211103.tar.gz 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz @@ -385,6 +386,7 @@ ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.tar.gz 0a7cab09dec357dab7819273f2542ff1c3ea0968 scala-2.13.6.tar.gz +1f8532dba290c6b2ef364632f3f92e71da93baba scala-2.13.7.tar.gz b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz 5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz diff -r d4ef127b74df -r d4a812e4f041 Admin/components/main --- a/Admin/components/main Tue Nov 02 13:51:29 2021 +0100 +++ b/Admin/components/main Wed Nov 03 10:44:54 2021 +0100 @@ -10,7 +10,7 @@ isabelle_fonts-20211004 isabelle_setup-20210922 jdk-17.0.1+12 -jedit-20211019 +jedit-20211103 jfreechart-1.5.3 jortho-1.0-2 kodkodi-1.5.7 @@ -19,7 +19,7 @@ opam-2.0.7 polyml-5.9-960de0cd0795 postgresql-42.2.24 -scala-2.13.5 +scala-2.13.7 smbc-0.4.1 spass-3.8ds-2 sqlite-jdbc-3.36.0.3 diff -r d4ef127b74df -r d4a812e4f041 NEWS --- a/NEWS Tue Nov 02 13:51:29 2021 +0100 +++ b/NEWS Wed Nov 03 10:44:54 2021 +0100 @@ -532,7 +532,8 @@ - sources of for the jEdit text editor and the Isabelle/jEdit plugins (jedit_base and jedit_main) are included by default, - more sources may be given on the command-line, - - options -f and -D make the tool more convenient. + - options -f and -D make the tool more convenient, + - Gradle has been replaced by Maven (less ambitious and more robust). * Remote provers from SystemOnTPTP (notably for Sledgehammer) are now managed via Isabelle/Scala instead of perl; the dependency on diff -r d4ef127b74df -r d4a812e4f041 src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Tue Nov 02 13:51:29 2021 +0100 +++ b/src/Doc/Main/Main_Doc.thy Wed Nov 03 10:44:54 2021 +0100 @@ -35,12 +35,12 @@ \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\\ (x = y)\ & @{term[source]"\ (x = y)"} & (\<^verbatim>\~=\)\\ @{term[source]"P \ Q"} & \<^term>\P \ Q\ \\ \<^term>\If x y z\ & @{term[source]"If x y z"}\\ \<^term>\Let e\<^sub>1 (\x. e\<^sub>2)\ & @{term[source]"Let e\<^sub>1 (\x. e\<^sub>2)"}\\ -\end{supertabular} +\end{tabular} \section*{Orderings} @@ -49,7 +49,7 @@ preorder, partial order, linear order, dense linear order and wellorder. \<^smallskip> -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\begin{tabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Orderings.less_eq\ & \<^typeof>\Orderings.less_eq\ & (\<^verbatim>\<=\)\\ \<^const>\Orderings.less\ & \<^typeof>\Orderings.less\\\ \<^const>\Orderings.Least\ & \<^typeof>\Orderings.Least\\\ @@ -60,11 +60,11 @@ @{const[source] bot} & \<^typeof>\Orderings.bot\\\ \<^const>\Orderings.mono\ & \<^typeof>\Orderings.mono\\\ \<^const>\Orderings.strict_mono\ & \<^typeof>\Orderings.strict_mono\\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} @{term[source]"x \ y"} & \<^term>\x \ y\ & (\<^verbatim>\>=\)\\ @{term[source]"x > y"} & \<^term>\x > y\\\ \<^term>\\x\y. P\ & @{term[source]"\x. x \ y \ P"}\\ @@ -72,7 +72,7 @@ \multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ \<^term>\LEAST x. P\ & @{term[source]"Least (\x. P)"}\\ \<^term>\GREATEST x. P\ & @{term[source]"Greatest (\x. P)"}\\ -\end{supertabular} +\end{tabular} \section*{Lattices} @@ -91,7 +91,7 @@ Available via \<^theory_text>\unbundle lattice_syntax\. -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} @{text[source]"x \ y"} & \<^term>\x \ y\\\ @{text[source]"x \ y"} & \<^term>\x < y\\\ @{text[source]"x \ y"} & \<^term>\inf x y\\\ @@ -100,12 +100,12 @@ @{text[source]"\A"} & \<^term>\Sup A\\\ @{text[source]"\"} & @{term[source] top}\\ @{text[source]"\"} & @{term[source] bot}\\ -\end{supertabular} +\end{tabular} \section*{Set} -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\begin{tabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Set.empty\ & @{term_type_only "Set.empty" "'a set"}\\ \<^const>\Set.insert\ & @{term_type_only insert "'a\'a set\'a set"}\\ \<^const>\Collect\ & @{term_type_only Collect "('a\bool)\'a set"}\\ @@ -119,11 +119,11 @@ \<^const>\image\ & @{term_type_only image "('a\'b)\'a set\'b set"}\\ \<^const>\Ball\ & @{term_type_only Ball "'a set$'a\bool)\bool"}\\ \<^const>\Bex\ & @{term_type_only Bex "'a set\('a\bool)\bool"}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \{a\<^sub>1,\,a\<^sub>n}\ & \insert a\<^sub>1 (\ (insert a\<^sub>n {})$\\\ \<^term>\a \ A\ & @{term[source]"\(x \ A)"}\\ \<^term>\A \ B\ & @{term[source]"A \ B"}\\ @@ -139,12 +139,12 @@ \<^term>\\x\A. P\ & @{term[source]"Ball A (\x. P)"}\\ \<^term>\\x\A. P\ & @{term[source]"Bex A (\x. P)"}\\ \<^term>\range f\ & @{term[source]"f ` UNIV"}\\ -\end{supertabular} +\end{tabular} \section*{Fun} -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\begin{tabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Fun.id\ & \<^typeof>\Fun.id\\\ \<^const>\Fun.comp\ & \<^typeof>\Fun.comp\ & (\texttt{o})\\ \<^const>\Fun.inj_on\ & @{term_type_only Fun.inj_on "('a\'b)\'a set\bool"}\\ @@ -153,7 +153,7 @@ \<^const>\Fun.bij\ & \<^typeof>\Fun.bij\\\ \<^const>\Fun.bij_betw\ & @{term_type_only Fun.bij_betw "('a\'b)\'a set\'b set\bool"}\\ \<^const>\Fun.fun_upd\ & \<^typeof>\Fun.fun_upd\\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} @@ -206,7 +206,7 @@ Types \<^typ>\unit\ and \\\. -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Product_Type.Unity\ & \<^typeof>\Product_Type.Unity\\\ \<^const>\Pair\ & \<^typeof>\Pair\\\ \<^const>\fst\ & \<^typeof>\fst\\\ @@ -214,7 +214,7 @@ \<^const>\case_prod\ & \<^typeof>\case_prod\\\ \<^const>\curry\ & \<^typeof>\curry\\\ \<^const>\Product_Type.Sigma\ & @{term_type_only Product_Type.Sigma "'a set\('a\'b set)\('a*'b)set"}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} @@ -264,13 +264,13 @@ \section*{Equiv\_Relations} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Equiv_Relations.equiv\ & @{term_type_only Equiv_Relations.equiv "'a set \ ('a*'a)set\bool"}\\ \<^const>\Equiv_Relations.quotient\ & @{term_type_only Equiv_Relations.quotient "'a set \ ('a \ 'a) set \ 'a set set"}\\ \<^const>\Equiv_Relations.congruent\ & @{term_type_only Equiv_Relations.congruent "('a*'a)set\('a\'b)\bool"}\\ \<^const>\Equiv_Relations.congruent2\ & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\('b*'b)set\('a\'b\'c)\bool"}\\ %@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} @@ -305,7 +305,7 @@ structures from semigroups up to fields. Everything is done in terms of overloaded operators: -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\begin{tabular}{@ {} l @ {~::~} l l @ {}} \0\ & \<^typeof>\zero\\\ \1\ & \<^typeof>\one\\\ \<^const>\plus\ & \<^typeof>\plus\\\ @@ -319,7 +319,7 @@ \<^const>\Rings.dvd\ & \<^typeof>\Rings.dvd\\\ \<^const>\divide\ & \<^typeof>\divide\\\ \<^const>\modulo\ & \<^typeof>\modulo\\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} @@ -394,53 +394,53 @@ \section*{Finite\_Set} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Finite_Set.finite\ & @{term_type_only Finite_Set.finite "'a set\bool"}\\ \<^const>\Finite_Set.card\ & @{term_type_only Finite_Set.card "'a set \ nat"}\\ \<^const>\Finite_Set.fold\ & @{term_type_only Finite_Set.fold "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b"}\\ -\end{supertabular} +\end{tabular} \section*{Lattices\_Big} -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\begin{tabular}{@ {} l @ {~::~} l l @ {}} \<^const>\Lattices_Big.Min\ & \<^typeof>\Lattices_Big.Min\\\ \<^const>\Lattices_Big.Max\ & \<^typeof>\Lattices_Big.Max\\\ \<^const>\Lattices_Big.arg_min\ & \<^typeof>\Lattices_Big.arg_min\\\ \<^const>\Lattices_Big.is_arg_min\ & \<^typeof>\Lattices_Big.is_arg_min\\\ \<^const>\Lattices_Big.arg_max\ & \<^typeof>\Lattices_Big.arg_max\\\ \<^const>\Lattices_Big.is_arg_max\ & \<^typeof>\Lattices_Big.is_arg_max\\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\ARG_MIN f x. P\ & @{term[source]"arg_min f (\x. P)"}\\ \<^term>\ARG_MAX f x. P\ & @{term[source]"arg_max f (\x. P)"}\\ -\end{supertabular} +\end{tabular} \section*{Groups\_Big} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Groups_Big.sum\ & @{term_type_only Groups_Big.sum "('a \ 'b) \ 'a set \ 'b::comm_monoid_add"}\\ \<^const>\Groups_Big.prod\ & @{term_type_only Groups_Big.prod "('a \ 'b) \ 'a set \ 'b::comm_monoid_mult"}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \<^term>\sum (\x. x) A\ & @{term[source]"sum (\x. x) A"} & (\<^verbatim>\SUM\)\\ \<^term>\sum (\x. t) A\ & @{term[source]"sum (\x. t) A"}\\ @{term[source] "\x|P. t"} & \<^term>\\x|P. t\\\ \multicolumn{2}{@ {}l@ {}}{Similarly for \\\ instead of \\\} & (\<^verbatim>\PROD\)\\ -\end{supertabular} +\end{tabular} \section*{Wellfounded} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Wellfounded.wf\ & @{term_type_only Wellfounded.wf "('a*'a)set\bool"}\\ \<^const>\Wellfounded.acc\ & @{term_type_only Wellfounded.acc "('a*'a)set\'a set"}\\ \<^const>\Wellfounded.measure\ & @{term_type_only Wellfounded.measure "('a\nat)\('a*'a)set"}\\ @@ -448,12 +448,12 @@ \<^const>\Wellfounded.mlex_prod\ & @{term_type_only Wellfounded.mlex_prod "('a\nat)\('a*'a)set\('a*'a)set"}\\ \<^const>\Wellfounded.less_than\ & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ \<^const>\Wellfounded.pred_nat\ & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ -\end{supertabular} +\end{tabular} \section*{Set\_Interval} % \<^theory>\HOL.Set_Interval\ -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\lessThan\ & @{term_type_only lessThan "'a::ord \ 'a set"}\\ \<^const>\atMost\ & @{term_type_only atMost "'a::ord \ 'a set"}\\ \<^const>\greaterThan\ & @{term_type_only greaterThan "'a::ord \ 'a set"}\\ @@ -462,11 +462,11 @@ \<^const>\atLeastLessThan\ & @{term_type_only atLeastLessThan "'a::ord \ 'a \ 'a set"}\\ \<^const>\greaterThanAtMost\ & @{term_type_only greaterThanAtMost "'a::ord \ 'a \ 'a set"}\\ \<^const>\atLeastAtMost\ & @{term_type_only atLeastAtMost "'a::ord \ 'a \ 'a set"}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \<^term>\lessThan y\ & @{term[source] "lessThan y"}\\ \<^term>\atMost y\ & @{term[source] "atMost y"}\\ \<^term>\greaterThan x\ & @{term[source] "greaterThan x"}\\ @@ -483,7 +483,7 @@ \<^term>\sum (\x. t) {..b}\ & @{term[source] "sum (\x. t) {..b}"}\\ \<^term>\sum (\x. t) {.. & @{term[source] "sum (\x. t) {..\\ instead of \\\}\\ -\end{supertabular} +\end{tabular} \section*{Power} @@ -564,13 +564,13 @@ \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} \[x\<^sub>1,\,x\<^sub>n]\ & \x\<^sub>1 # \ # x\<^sub>n # []\\\ \<^term>\[m.. & @{term[source]"upt m n"}\\ \<^term>\[i..j]\ & @{term[source]"upto i j"}\\ \<^term>\xs[n := x]\ & @{term[source]"list_update xs n x"}\\ \<^term>\\x\xs. e\ & @{term[source]"listsum (map (\x. e) xs)"}\\ -\end{supertabular} +\end{tabular} \<^medskip> Filter input syntax \[pat \ e. b]\, where @@ -585,7 +585,7 @@ Maps model partial functions and are often used as finite tables. However, the domain of a map may be infinite. -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \<^const>\Map.empty\ & \<^typeof>\Map.empty\\\ \<^const>\Map.map_add\ & \<^typeof>\Map.map_add\\\ \<^const>\Map.map_comp\ & \<^typeof>\