# HG changeset patch
# User wenzelm
# Date 1594823306 -7200
# Node ID c6756adfef0f80b7572d59a76899ff1d449ab1e0
# Parent  08f1e4cb735fd3fe7cabc4d5ab471cfafb010845# Parent  254c324f31fd1572c1a34dad3966e7e7480dc812
merged

diff -r 08f1e4cb735f -r c6756adfef0f src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Doc/Implementation/Integration.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -131,7 +131,7 @@
 \<close>
 
 text %mlex \<open>
-  The file \<^file>\<open>~~/src/HOL/ex/Commands.thy\<close> shows some example Isar command
+  The file \<^file>\<open>~~/src/HOL/Examples/Commands.thy\<close> shows some example Isar command
   definitions, with the all-important theory header declarations for outer
   syntax keywords.
 \<close>
diff -r 08f1e4cb735f -r c6756adfef0f src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -543,7 +543,7 @@
   \<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
   from well-founded induction and completeness of patterns. This factors out
   some operations that are done internally by the function package and makes
-  them available separately. See \<^file>\<open>~~/src/HOL/ex/Induction_Schema.thy\<close> for
+  them available separately. See \<^file>\<open>~~/src/HOL/Examples/Induction_Schema.thy\<close> for
   examples.
 \<close>
 
@@ -662,7 +662,7 @@
   Adhoc overloading allows to overload a constant depending on its type.
   Typically this involves the introduction of an uninterpreted constant (used
   for input and output) and the addition of some variants (used internally).
-  For examples see \<^file>\<open>~~/src/HOL/ex/Adhoc_Overloading_Examples.thy\<close> and
+  For examples see \<^file>\<open>~~/src/HOL/Examples/Adhoc_Overloading_Examples.thy\<close> and
   \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
 
   \<^rail>\<open>
@@ -1010,7 +1010,7 @@
 
 subsubsection \<open>Examples\<close>
 
-text \<open>See \<^file>\<open>~~/src/HOL/ex/Records.thy\<close>, for example.\<close>
+text \<open>See \<^file>\<open>~~/src/HOL/Examples/Records.thy\<close>, for example.\<close>
 
 
 section \<open>Semantic subtype definitions \label{sec:hol-typedef}\<close>
@@ -2150,7 +2150,7 @@
 (*<*)end(*>*)
 
 text \<open>
-  See also \<^file>\<open>~~/src/HOL/ex/Groebner_Examples.thy\<close>.
+  See also \<^file>\<open>~~/src/HOL/Examples/Groebner_Examples.thy\<close>.
 \<close>
 
 
@@ -2167,7 +2167,7 @@
 
   \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> @{cite
   "Bezem-Coquand:2005"}, which covers applications in confluence theory,
-  lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/ex/Coherent.thy\<close>
+  lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/Examples/Coherent.thy\<close>
   for some examples.
 \<close>
 
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -15,7 +15,7 @@
   "HOL-Computational_Algebra.Computational_Algebra"
   "HOL-Computational_Algebra.Polynomial_Factorial"
   "HOL-Number_Theory.Eratosthenes"
-  "HOL-ex.Records"
+  "HOL-Examples.Records"
   "HOL-Word.Word"
 begin
 
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/Examples/Ackermann.thy
--- a/src/HOL/Examples/Ackermann.thy	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/HOL/Examples/Ackermann.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -1,3 +1,7 @@
+(*  Title:      HOL/Examples/Ackermann.thy
+    Author:     Larry Paulson
+*)
+
 section \<open>A Tail-Recursive, Stack-Based Ackermann's Function\<close>
 
 theory Ackermann imports Main
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/Examples/Adhoc_Overloading_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Adhoc_Overloading_Examples.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -0,0 +1,256 @@
+(*  Title:      HOL/Examples/Adhoc_Overloading_Examples.thy
+    Author:     Christian Sternagel
+*)
+
+section \<open>Ad Hoc Overloading\<close>
+
+theory Adhoc_Overloading_Examples
+imports
+  Main
+  "HOL-Library.Infinite_Set"
+  "HOL-Library.Adhoc_Overloading"
+begin
+
+text \<open>Adhoc overloading allows to overload a constant depending on
+its type. Typically this involves to introduce an uninterpreted
+constant (used for input and output) and then add some variants (used
+internally).\<close>
+
+subsection \<open>Plain Ad Hoc Overloading\<close>
+
+text \<open>Consider the type of first-order terms.\<close>
+datatype ('a, 'b) "term" =
+  Var 'b |
+  Fun 'a "('a, 'b) term list"
+
+text \<open>The set of variables of a term might be computed as follows.\<close>
+fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where
+  "term_vars (Var x) = {x}" |
+  "term_vars (Fun f ts) = \<Union>(set (map term_vars ts))"
+
+text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
+rewrite systems (i.e., sets of rules), the set of variables makes
+sense. Thus we introduce an unspecified constant \<open>vars\<close>.\<close>
+
+consts vars :: "'a \<Rightarrow> 'b set"
+
+text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close>
+adhoc_overloading
+  vars term_vars
+
+value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
+
+fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
+  "rule_vars (l, r) = vars l \<union> vars r"
+
+adhoc_overloading
+  vars rule_vars
+
+value [nbe] "vars (Var 1, Var 0)"
+
+definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
+  "trs_vars R = \<Union>(rule_vars ` R)"
+
+adhoc_overloading
+  vars trs_vars
+
+value [nbe] "vars {(Var 1, Var 0)}"
+
+text \<open>Sometimes it is necessary to add explicit type constraints
+before a variant can be determined.\<close>
+(*value "vars R" (*has multiple instances*)*)
+value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)"
+
+text \<open>It is also possible to remove variants.\<close>
+no_adhoc_overloading
+  vars term_vars rule_vars 
+
+(*value "vars (Var 1)" (*does not have an instance*)*)
+
+text \<open>As stated earlier, the overloaded constant is only used for
+input and output. Internally, always a variant is used, as can be
+observed by the configuration option \<open>show_variants\<close>.\<close>
+
+adhoc_overloading
+  vars term_vars
+
+declare [[show_variants]]
+
+term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*)
+
+
+subsection \<open>Adhoc Overloading inside Locales\<close>
+
+text \<open>As example we use permutations that are parametrized over an
+atom type \<^typ>\<open>'a\<close>.\<close>
+
+definition perms :: "('a \<Rightarrow> 'a) set" where
+  "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
+
+typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
+  by standard (auto simp: perms_def)
+
+text \<open>First we need some auxiliary lemmas.\<close>
+lemma permsI [Pure.intro]:
+  assumes "bij f" and "MOST x. f x = x"
+  shows "f \<in> perms"
+  using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg)
+
+lemma perms_imp_bij:
+  "f \<in> perms \<Longrightarrow> bij f"
+  by (simp add: perms_def)
+
+lemma perms_imp_MOST_eq:
+  "f \<in> perms \<Longrightarrow> MOST x. f x = x"
+  by (simp add: perms_def) (metis MOST_iff_finiteNeg)
+
+lemma id_perms [simp]:
+  "id \<in> perms"
+  "(\<lambda>x. x) \<in> perms"
+  by (auto simp: perms_def bij_def)
+
+lemma perms_comp [simp]:
+  assumes f: "f \<in> perms" and g: "g \<in> perms"
+  shows "(f \<circ> g) \<in> perms"
+  apply (intro permsI bij_comp)
+  apply (rule perms_imp_bij [OF g])
+  apply (rule perms_imp_bij [OF f])
+  apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]])
+  apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]])
+  by simp
+
+lemma perms_inv:
+  assumes f: "f \<in> perms"
+  shows "inv f \<in> perms"
+  apply (rule permsI)
+  apply (rule bij_imp_bij_inv)
+  apply (rule perms_imp_bij [OF f])
+  apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]])
+  apply (erule subst, rule inv_f_f)
+  apply (rule bij_is_inj [OF perms_imp_bij [OF f]])
+  done
+
+lemma bij_Rep_perm: "bij (Rep_perm p)"
+  using Rep_perm [of p] unfolding perms_def by simp
+
+instantiation perm :: (type) group_add
+begin
+
+definition "0 = Abs_perm id"
+definition "- p = Abs_perm (inv (Rep_perm p))"
+definition "p + q = Abs_perm (Rep_perm p \<circ> Rep_perm q)"
+definition "(p1::'a perm) - p2 = p1 + - p2"
+
+lemma Rep_perm_0: "Rep_perm 0 = id"
+  unfolding zero_perm_def by (simp add: Abs_perm_inverse)
+
+lemma Rep_perm_add:
+  "Rep_perm (p1 + p2) = Rep_perm p1 \<circ> Rep_perm p2"
+  unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm)
+
+lemma Rep_perm_uminus:
+  "Rep_perm (- p) = inv (Rep_perm p)"
+  unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)
+
+instance
+  apply standard
+  unfolding Rep_perm_inject [symmetric]
+  unfolding minus_perm_def
+  unfolding Rep_perm_add
+  unfolding Rep_perm_uminus
+  unfolding Rep_perm_0
+  apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
+  done
+
+end
+
+lemmas Rep_perm_simps =
+  Rep_perm_0
+  Rep_perm_add
+  Rep_perm_uminus
+
+
+section \<open>Permutation Types\<close>
+
+text \<open>We want to be able to apply permutations to arbitrary types. To
+this end we introduce a constant \<open>PERMUTE\<close> together with
+convenient infix syntax.\<close>
+
+consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "\<bullet>" 75)
+
+text \<open>Then we add a locale for types \<^typ>\<open>'b\<close> that support
+appliciation of permutations.\<close>
+locale permute =
+  fixes permute :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
+  assumes permute_zero [simp]: "permute 0 x = x"
+    and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)"
+begin
+
+adhoc_overloading
+  PERMUTE permute
+
+end
+
+text \<open>Permuting atoms.\<close>
+definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where
+  "permute_atom p a = (Rep_perm p) a"
+
+adhoc_overloading
+  PERMUTE permute_atom
+
+interpretation atom_permute: permute permute_atom
+  by standard (simp_all add: permute_atom_def Rep_perm_simps)
+
+text \<open>Permuting permutations.\<close>
+definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
+  "permute_perm p q = p + q - p"
+
+adhoc_overloading
+  PERMUTE permute_perm
+
+interpretation perm_permute: permute permute_perm
+  apply standard
+  unfolding permute_perm_def
+  apply simp
+  apply (simp only: diff_conv_add_uminus minus_add add.assoc)
+  done
+
+text \<open>Permuting functions.\<close>
+locale fun_permute =
+  dom: permute perm1 + ran: permute perm2
+  for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
+  and perm2 :: "'a perm \<Rightarrow> 'c \<Rightarrow> 'c"
+begin
+
+adhoc_overloading
+  PERMUTE perm1 perm2
+
+definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where
+  "permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))"
+
+adhoc_overloading
+  PERMUTE permute_fun
+
+end
+
+sublocale fun_permute \<subseteq> permute permute_fun
+  by (unfold_locales, auto simp: permute_fun_def)
+     (metis dom.permute_plus minus_add)
+
+lemma "(Abs_perm id :: nat perm) \<bullet> Suc 0 = Suc 0"
+  unfolding permute_atom_def
+  by (metis Rep_perm_0 id_apply zero_perm_def)
+
+interpretation atom_fun_permute: fun_permute permute_atom permute_atom
+  by (unfold_locales)
+
+adhoc_overloading
+  PERMUTE atom_fun_permute.permute_fun
+
+lemma "(Abs_perm id :: 'a perm) \<bullet> id = id"
+  unfolding atom_fun_permute.permute_fun_def
+  unfolding permute_atom_def
+  by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def)
+
+end
+
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/Examples/Coherent.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Coherent.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -0,0 +1,95 @@
+(*  Title:      HOL/Examples/Coherent.thy
+    Author:     Stefan Berghofer, TU Muenchen
+    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
+*)
+
+section \<open>Coherent Logic Problems\<close>
+
+theory Coherent
+imports Main
+begin
+
+subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
+
+no_notation
+  comp (infixl "o" 55) and
+  relcomp (infixr "O" 75)
+
+lemma p1p2:
+  assumes "col a b c l \<and> col d e f m"
+    and "col b f g n \<and> col c e g o"
+    and "col b d h p \<and> col a e h q"
+    and "col c d i r \<and> col a f i s"
+    and "el n o \<Longrightarrow> goal"
+    and "el p q \<Longrightarrow> goal"
+    and "el s r \<Longrightarrow> goal"
+    and "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
+    and "\<And>A B. pl A B \<Longrightarrow> ep A A"
+    and "\<And>A B. ep A B \<Longrightarrow> ep B A"
+    and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
+    and "\<And>A B. pl A B \<Longrightarrow> el B B"
+    and "\<And>A B. el A B \<Longrightarrow> el B A"
+    and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
+    and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
+    and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
+    and "\<And>A B C D E F G H I J K L M N O P Q.
+           col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
+           col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
+           (\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> pl G D"
+    and "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C"
+    and "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
+  shows goal using assms
+  by coherent
+
+lemma p2p1:
+  assumes "col a b c l \<and> col d e f m"
+    and "col b f g n \<and> col c e g o"
+    and "col b d h p \<and> col a e h q"
+    and "col c d i r \<and> col a f i s"
+    and "pl a m \<Longrightarrow> goal"
+    and "pl b m \<Longrightarrow> goal"
+    and "pl c m \<Longrightarrow> goal"
+    and "pl d l \<Longrightarrow> goal"
+    and "pl e l \<Longrightarrow> goal"
+    and "pl f l \<Longrightarrow> goal"
+    and "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
+    and "\<And>A B. pl A B \<Longrightarrow> ep A A"
+    and "\<And>A B. ep A B \<Longrightarrow> ep B A"
+    and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
+    and "\<And>A B. pl A B \<Longrightarrow> el B B"
+    and "\<And>A B. el A B \<Longrightarrow> el B A"
+    and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
+    and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
+    and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
+    and "\<And>A B C D E F G H I J K L M N O P Q.
+           col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
+           col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
+           (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
+    and "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B"
+    and "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
+  shows goal using assms
+  by coherent
+
+
+subsection \<open>Preservation of the Diamond Property under reflexive closure\<close>
+
+lemma diamond:
+  assumes "reflexive_rewrite a b" "reflexive_rewrite a c"
+    and "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
+    and "\<And>A. equalish A A" 
+    and "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
+    and "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
+    and "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
+    and "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
+    and "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
+    and "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
+  shows goal using assms
+  by coherent
+
+end
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/Examples/Commands.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Commands.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -0,0 +1,77 @@
+(*  Title:      HOL/Examples/Commands.thy
+    Author:     Makarius
+*)
+
+section \<open>Some Isar command definitions\<close>
+
+theory Commands
+imports Main
+keywords
+  "print_test" :: diag and
+  "global_test" :: thy_decl and
+  "local_test" :: thy_decl
+begin
+
+subsection \<open>Diagnostic command: no state change\<close>
+
+ML \<open>
+  Outer_Syntax.command \<^command_keyword>\<open>print_test\<close> "print term test"
+    (Parse.term >> (fn s => Toplevel.keep (fn st =>
+      let
+        val ctxt = Toplevel.context_of st;
+        val t = Syntax.read_term ctxt s;
+        val ctxt' = Proof_Context.augment t ctxt;
+      in Pretty.writeln (Syntax.pretty_term ctxt' t) end)));
+\<close>
+
+print_test x
+print_test "\<lambda>x. x = a"
+
+
+subsection \<open>Old-style global theory declaration\<close>
+
+ML \<open>
+  Outer_Syntax.command \<^command_keyword>\<open>global_test\<close> "test constant declaration"
+    (Parse.binding >> (fn b => Toplevel.theory (fn thy =>
+      let
+        val thy' = Sign.add_consts [(b, \<^typ>\<open>'a\<close>, NoSyn)] thy;
+      in thy' end)));
+\<close>
+
+global_test a
+global_test b
+print_test a
+
+
+subsection \<open>Local theory specification\<close>
+
+ML \<open>
+  Outer_Syntax.local_theory \<^command_keyword>\<open>local_test\<close> "test local definition"
+    (Parse.binding -- (\<^keyword>\<open>=\<close> |-- Parse.term) >> (fn (b, s) => fn lthy =>
+      let
+        val t = Syntax.read_term lthy s;
+        val (def, lthy') = Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), t)) lthy;
+      in lthy' end));
+\<close>
+
+local_test true = True
+print_test true
+thm true_def
+
+local_test identity = "\<lambda>x. x"
+print_test "identity x"
+thm identity_def
+
+context fixes x y :: nat
+begin
+
+local_test test = "x + y"
+print_test test
+thm test_def
+
+end
+
+print_test "test 0 1"
+thm test_def
+
+end
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/Examples/Groebner_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Groebner_Examples.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -0,0 +1,116 @@
+(*  Title:      HOL/Examples/Groebner_Examples.thy
+    Author:     Amine Chaieb, TU Muenchen
+*)
+
+section \<open>Groebner Basis Examples\<close>
+
+theory Groebner_Examples
+imports Main
+begin
+
+subsection \<open>Basic examples\<close>
+
+lemma
+  fixes x :: int
+  shows "x ^ 3 = x ^ 3"
+  apply (tactic \<open>ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
+  by (rule refl)
+
+lemma
+  fixes x :: int
+  shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<^sup>2 + (80 * x + 32))))" 
+  apply (tactic \<open>ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
+  by (rule refl)
+
+schematic_goal
+  fixes x :: int
+  shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X" 
+  apply (tactic \<open>ALLGOALS (CONVERSION
+    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
+  by (rule refl)
+
+lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{comm_ring_1})"
+  apply (simp only: power_Suc power_0)
+  apply (simp only: semiring_norm)
+  oops
+
+lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"
+  by algebra
+
+lemma "(4::nat) + 4 = 3 + 5"
+  by algebra
+
+lemma "(4::int) + 0 = 4"
+  apply algebra?
+  by simp
+
+lemma
+  assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0"
+  shows "d\<^sup>2 * c\<^sup>2 - 2 * d * c * a * f + a\<^sup>2 * f\<^sup>2 - e * d * b * c - e * b * a * f +
+    a * e\<^sup>2 * c + f * d * b\<^sup>2 = 0"
+  using assms by algebra
+
+lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
+  by algebra
+
+theorem "x* (x\<^sup>2 - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
+  by algebra
+
+lemma
+  fixes x::"'a::idom"
+  shows "x\<^sup>2*y = x\<^sup>2 & x*y\<^sup>2 = y\<^sup>2 \<longleftrightarrow>  x = 1 & y = 1 | x = 0 & y = 0"
+  by algebra
+
+subsection \<open>Lemmas for Lagrange's theorem\<close>
+
+definition
+  sq :: "'a::times => 'a" where
+  "sq x == x*x"
+
+lemma
+  fixes x1 :: "'a::{idom}"
+  shows
+  "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
+    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
+    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
+    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
+    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
+  by (algebra add: sq_def)
+
+lemma
+  fixes p1 :: "'a::{idom}"
+  shows
+  "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
+   (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
+    = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
+      sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
+      sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
+      sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
+      sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
+      sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
+      sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
+      sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
+  by (algebra add: sq_def)
+
+
+subsection \<open>Colinearity is invariant by rotation\<close>
+
+type_synonym point = "int \<times> int"
+
+definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
+  "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
+    ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"
+
+lemma collinear_inv_rotation:
+  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
+  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
+    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
+  using assms 
+  by (algebra add: collinear_def split_def fst_conv snd_conv)
+
+lemma "\<exists>(d::int). a*y - a*x = n*d \<Longrightarrow> \<exists>u v. a*u + n*v = 1 \<Longrightarrow> \<exists>e. y - x = n*e"
+  by algebra
+
+end
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/Examples/Iff_Oracle.thy
--- a/src/HOL/Examples/Iff_Oracle.thy	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/HOL/Examples/Iff_Oracle.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Example/Iff_Oracle.thy
+(*  Title:      HOL/Examples/Iff_Oracle.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Makarius
 *)
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/Examples/Induction_Schema.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Induction_Schema.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -0,0 +1,48 @@
+(*  Title:      HOL/Examples/Induction_Schema.thy
+    Author:     Alexander Krauss, TU Muenchen
+*)
+
+section \<open>Examples of automatically derived induction rules\<close>
+
+theory Induction_Schema
+imports Main
+begin
+
+subsection \<open>Some simple induction principles on nat\<close>
+
+lemma nat_standard_induct: (* cf. Nat.thy *)
+  "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma nat_induct2:
+  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
+  \<Longrightarrow> P n"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma minus_one_induct:
+  "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x"
+by induction_schema (pat_completeness, lexicographic_order)
+
+theorem diff_induct: (* cf. Nat.thy *)
+  "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
+    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma list_induct2': (* cf. List.thy *)
+  "\<lbrakk> P [] [];
+  \<And>x xs. P (x#xs) [];
+  \<And>y ys. P [] (y#ys);
+   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
+ \<Longrightarrow> P xs ys"
+by induction_schema (pat_completeness, lexicographic_order)
+
+theorem even_odd_induct:
+  assumes "R 0"
+  assumes "Q 0"
+  assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)"
+  assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)"
+  shows "R n" "Q n"
+  using assms
+by induction_schema (pat_completeness+, lexicographic_order)
+
+end
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/Examples/Records.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Examples/Records.thy	Wed Jul 15 16:28:26 2020 +0200
@@ -0,0 +1,329 @@
+(*  Title:      HOL/Examples/Records.thy
+    Author:     Wolfgang Naraschewski, TU Muenchen
+    Author:     Norbert Schirmer, TU Muenchen
+    Author:     Markus Wenzel, TU Muenchen
+*)
+
+section \<open>Using extensible records in HOL -- points and coloured points\<close>
+
+theory Records
+  imports Main
+begin
+
+subsection \<open>Points\<close>
+
+record point =
+  xpos :: nat
+  ypos :: nat
+
+text \<open>
+  Apart many other things, above record declaration produces the
+  following theorems:
+\<close>
+
+thm point.simps
+thm point.iffs
+thm point.defs
+
+text \<open>
+  The set of theorems @{thm [source] point.simps} is added
+  automatically to the standard simpset, @{thm [source] point.iffs} is
+  added to the Classical Reasoner and Simplifier context.
+
+  \<^medskip> Record declarations define new types and type abbreviations:
+  @{text [display]
+\<open>point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
+'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type\<close>}
+\<close>
+
+consts foo2 :: "\<lparr>xpos :: nat, ypos :: nat\<rparr>"
+consts foo4 :: "'a \<Rightarrow> \<lparr>xpos :: nat, ypos :: nat, \<dots> :: 'a\<rparr>"
+
+
+subsubsection \<open>Introducing concrete records and record schemes\<close>
+
+definition foo1 :: point
+  where "foo1 = \<lparr>xpos = 1, ypos = 0\<rparr>"
+
+definition foo3 :: "'a \<Rightarrow> 'a point_scheme"
+  where "foo3 ext = \<lparr>xpos = 1, ypos = 0, \<dots> = ext\<rparr>"
+
+
+subsubsection \<open>Record selection and record update\<close>
+
+definition getX :: "'a point_scheme \<Rightarrow> nat"
+  where "getX r = xpos r"
+
+definition setX :: "'a point_scheme \<Rightarrow> nat \<Rightarrow> 'a point_scheme"
+  where "setX r n = r \<lparr>xpos := n\<rparr>"
+
+
+subsubsection \<open>Some lemmas about records\<close>
+
+text \<open>Basic simplifications.\<close>
+
+lemma "point.make n p = \<lparr>xpos = n, ypos = p\<rparr>"
+  by (simp only: point.make_def)
+
+lemma "xpos \<lparr>xpos = m, ypos = n, \<dots> = p\<rparr> = m"
+  by simp
+
+lemma "\<lparr>xpos = m, ypos = n, \<dots> = p\<rparr>\<lparr>xpos:= 0\<rparr> = \<lparr>xpos = 0, ypos = n, \<dots> = p\<rparr>"
+  by simp
+
+
+text \<open>\<^medskip> Equality of records.\<close>
+
+lemma "n = n' \<Longrightarrow> p = p' \<Longrightarrow> \<lparr>xpos = n, ypos = p\<rparr> = \<lparr>xpos = n', ypos = p'\<rparr>"
+  \<comment> \<open>introduction of concrete record equality\<close>
+  by simp
+
+lemma "\<lparr>xpos = n, ypos = p\<rparr> = \<lparr>xpos = n', ypos = p'\<rparr> \<Longrightarrow> n = n'"
+  \<comment> \<open>elimination of concrete record equality\<close>
+  by simp
+
+lemma "r\<lparr>xpos := n\<rparr>\<lparr>ypos := m\<rparr> = r\<lparr>ypos := m\<rparr>\<lparr>xpos := n\<rparr>"
+  \<comment> \<open>introduction of abstract record equality\<close>
+  by simp
+
+lemma "r\<lparr>xpos := n\<rparr> = r\<lparr>xpos := n'\<rparr>" if "n = n'"
+  \<comment> \<open>elimination of abstract record equality (manual proof)\<close>
+proof -
+  let "?lhs = ?rhs" = ?thesis
+  from that have "xpos ?lhs = xpos ?rhs" by simp
+  then show ?thesis by simp
+qed
+
+
+text \<open>\<^medskip> Surjective pairing\<close>
+
+lemma "r = \<lparr>xpos = xpos r, ypos = ypos r\<rparr>"
+  by simp
+
+lemma "r = \<lparr>xpos = xpos r, ypos = ypos r, \<dots> = point.more r\<rparr>"
+  by simp
+
+
+text \<open>\<^medskip> Representation of records by cases or (degenerate) induction.\<close>
+
+lemma "r\<lparr>xpos := n\<rparr>\<lparr>ypos := m\<rparr> = r\<lparr>ypos := m\<rparr>\<lparr>xpos := n\<rparr>"
+proof (cases r)
+  fix xpos ypos more
+  assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>"
+  then show ?thesis by simp
+qed
+
+lemma "r\<lparr>xpos := n\<rparr>\<lparr>ypos := m\<rparr> = r\<lparr>ypos := m\<rparr>\<lparr>xpos := n\<rparr>"
+proof (induct r)
+  fix xpos ypos more
+  show "\<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>\<lparr>xpos := n, ypos := m\<rparr> =
+      \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>\<lparr>ypos := m, xpos := n\<rparr>"
+    by simp
+qed
+
+lemma "r\<lparr>xpos := n\<rparr>\<lparr>xpos := m\<rparr> = r\<lparr>xpos := m\<rparr>"
+proof (cases r)
+  fix xpos ypos more
+  assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>"
+  then show ?thesis by simp
+qed
+
+lemma "r\<lparr>xpos := n\<rparr>\<lparr>xpos := m\<rparr> = r\<lparr>xpos := m\<rparr>"
+proof (cases r)
+  case fields
+  then show ?thesis by simp
+qed
+
+lemma "r\<lparr>xpos := n\<rparr>\<lparr>xpos := m\<rparr> = r\<lparr>xpos := m\<rparr>"
+  by (cases r) simp
+
+
+text \<open>\<^medskip> Concrete records are type instances of record schemes.\<close>
+
+definition foo5 :: nat
+  where "foo5 = getX \<lparr>xpos = 1, ypos = 0\<rparr>"
+
+
+text \<open>\<^medskip> Manipulating the ``\<open>...\<close>'' (more) part.\<close>
+
+definition incX :: "'a point_scheme \<Rightarrow> 'a point_scheme"
+  where "incX r = \<lparr>xpos = xpos r + 1, ypos = ypos r, \<dots> = point.more r\<rparr>"
+
+lemma "incX r = setX r (Suc (getX r))"
+  by (simp add: getX_def setX_def incX_def)
+
+
+text \<open>\<^medskip> An alternative definition.\<close>
+
+definition incX' :: "'a point_scheme \<Rightarrow> 'a point_scheme"
+  where "incX' r = r\<lparr>xpos := xpos r + 1\<rparr>"
+
+
+subsection \<open>Coloured points: record extension\<close>
+
+datatype colour = Red | Green | Blue
+
+record cpoint = point +
+  colour :: colour
+
+
+text \<open>
+  The record declaration defines a new type constructor and abbreviations:
+  @{text [display]
+\<open>cpoint = \<lparr>xpos :: nat, ypos :: nat, colour :: colour\<rparr> =
+  () cpoint_ext_type point_ext_type
+'a cpoint_scheme = \<lparr>xpos :: nat, ypos :: nat, colour :: colour, \<dots> :: 'a\<rparr> =
+  'a cpoint_ext_type point_ext_type\<close>}
+\<close>
+
+consts foo6 :: cpoint
+consts foo7 :: "\<lparr>xpos :: nat, ypos :: nat, colour :: colour\<rparr>"
+consts foo8 :: "'a cpoint_scheme"
+consts foo9 :: "\<lparr>xpos :: nat, ypos :: nat, colour :: colour, \<dots> :: 'a\<rparr>"
+
+
+text \<open>Functions on \<open>point\<close> schemes work for \<open>cpoints\<close> as well.\<close>
+
+definition foo10 :: nat
+  where "foo10 = getX \<lparr>xpos = 2, ypos = 0, colour = Blue\<rparr>"
+
+
+subsubsection \<open>Non-coercive structural subtyping\<close>
+
+text \<open>Term \<^term>\<open>foo11\<close> has type \<^typ>\<open>cpoint\<close>, not type \<^typ>\<open>point\<close> --- Great!\<close>
+
+definition foo11 :: cpoint
+  where "foo11 = setX \<lparr>xpos = 2, ypos = 0, colour = Blue\<rparr> 0"
+
+
+subsection \<open>Other features\<close>
+
+text \<open>Field names contribute to record identity.\<close>
+
+record point' =
+  xpos' :: nat
+  ypos' :: nat
+
+text \<open>
+  \<^noindent> May not apply \<^term>\<open>getX\<close> to @{term [source] "\<lparr>xpos' = 2, ypos' = 0\<rparr>"}
+  --- type error.
+\<close>
+
+text \<open>\<^medskip> Polymorphic records.\<close>
+
+record 'a point'' = point +
+  content :: 'a
+
+type_synonym cpoint'' = "colour point''"
+
+
+text \<open>Updating a record field with an identical value is simplified.\<close>
+lemma "r\<lparr>xpos := xpos r\<rparr> = r"
+  by simp
+
+text \<open>Only the most recent update to a component survives simplification.\<close>
+lemma "r\<lparr>xpos := x, ypos := y, xpos := x'\<rparr> = r\<lparr>ypos := y, xpos := x'\<rparr>"
+  by simp
+
+text \<open>
+  In some cases its convenient to automatically split (quantified) records.
+  For this purpose there is the simproc @{ML [source] "Record.split_simproc"}
+  and the tactic @{ML [source] "Record.split_simp_tac"}. The simplification
+  procedure only splits the records, whereas the tactic also simplifies the
+  resulting goal with the standard record simplification rules. A
+  (generalized) predicate on the record is passed as parameter that decides
+  whether or how `deep' to split the record. It can peek on the subterm
+  starting at the quantified occurrence of the record (including the
+  quantifier). The value \<^ML>\<open>0\<close> indicates no split, a value greater
+  \<^ML>\<open>0\<close> splits up to the given bound of record extension and finally the
+  value \<^ML>\<open>~1\<close> completely splits the record. @{ML [source]
+  "Record.split_simp_tac"} additionally takes a list of equations for
+  simplification and can also split fixed record variables.
+\<close>
+
+lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
+  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
+    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+  apply simp
+  done
+
+lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
+  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
+  apply simp
+  done
+
+lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
+  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
+    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+  apply simp
+  done
+
+lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
+  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
+  apply simp
+  done
+
+lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
+    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+  apply auto
+  done
+
+lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
+  apply auto
+  done
+
+lemma "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
+  apply auto
+  done
+
+notepad
+begin
+  have "\<exists>x. P x"
+    if "P (xpos r)" for P r
+    apply (insert that)
+    apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
+    apply auto
+    done
+end
+
+text \<open>
+  The effect of simproc @{ML [source] Record.ex_sel_eq_simproc} is illustrated
+  by the following lemma.\<close>
+
+lemma "\<exists>r. xpos r = x"
+  by (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
+    addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>)
+
+
+subsection \<open>A more complex record expression\<close>
+
+record ('a, 'b, 'c) bar = bar1 :: 'a
+  bar2 :: 'b
+  bar3 :: 'c
+  bar21 :: "'b \<times> 'a"
+  bar32 :: "'c \<times> 'b"
+  bar31 :: "'c \<times> 'a"
+
+print_record "('a,'b,'c) bar"
+
+
+subsection \<open>Some code generation\<close>
+
+export_code foo1 foo3 foo5 foo10 checking SML
+
+text \<open>
+  Code generation can also be switched off, for instance for very large
+  records:\<close>
+
+declare [[record_codegen = false]]
+
+record not_so_large_record =
+  bar520 :: nat
+  bar521 :: "nat \<times> nat"
+
+declare [[record_codegen = true]]
+
+end
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/HOL/ROOT	Wed Jul 15 16:28:26 2020 +0200
@@ -20,14 +20,20 @@
   sessions
     "HOL-Library"
   theories
+    Adhoc_Overloading_Examples
     Ackermann
-    Knaster_Tarski
-    Peirce
+    Cantor
+    Coherent
+    Commands
     Drinker
-    Cantor
+    Groebner_Examples
+    Iff_Oracle
+    Induction_Schema
+    Knaster_Tarski
+    "ML"
+    Peirce
+    Records
     Seq
-    "ML"
-    Iff_Oracle
   document_files
     "root.bib"
     "root.tex"
@@ -605,7 +611,6 @@
     Miscellaneous examples for Higher-Order Logic.
   "
   theories
-    Adhoc_Overloading_Examples
     Antiquote
     Argo_Examples
     Arith_Examples
@@ -623,8 +628,6 @@
     Code_Lazy_Demo
     Code_Timing
     Coercion_Examples
-    Coherent
-    Commands
     Computations
     Conditional_Parametricity_Examples
     Cubic_Quartic
@@ -637,13 +640,11 @@
     Functions
     Function_Growth
     Gauge_Integration
-    Groebner_Examples
     Guess
     HarmonicSeries
     Hebrew
     Hex_Bin_Examples
     IArray_Examples
-    Induction_Schema
     Intuitionistic
     Join_Theory
     Lagrange
@@ -663,7 +664,6 @@
     Pythagoras
     Quicksort
     Radix_Sort
-    Records
     Reflection_Examples
     Refute_Examples
     Residue_Ring
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Mon Jul 13 15:23:32 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-(*  Title:      HOL/ex/Adhoc_Overloading_Examples.thy
-    Author:     Christian Sternagel
-*)
-
-section \<open>Ad Hoc Overloading\<close>
-
-theory Adhoc_Overloading_Examples
-imports
-  Main
-  "HOL-Library.Infinite_Set"
-  "HOL-Library.Adhoc_Overloading"
-begin
-
-text \<open>Adhoc overloading allows to overload a constant depending on
-its type. Typically this involves to introduce an uninterpreted
-constant (used for input and output) and then add some variants (used
-internally).\<close>
-
-subsection \<open>Plain Ad Hoc Overloading\<close>
-
-text \<open>Consider the type of first-order terms.\<close>
-datatype ('a, 'b) "term" =
-  Var 'b |
-  Fun 'a "('a, 'b) term list"
-
-text \<open>The set of variables of a term might be computed as follows.\<close>
-fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where
-  "term_vars (Var x) = {x}" |
-  "term_vars (Fun f ts) = \<Union>(set (map term_vars ts))"
-
-text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
-rewrite systems (i.e., sets of rules), the set of variables makes
-sense. Thus we introduce an unspecified constant \<open>vars\<close>.\<close>
-
-consts vars :: "'a \<Rightarrow> 'b set"
-
-text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close>
-adhoc_overloading
-  vars term_vars
-
-value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
-
-fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
-  "rule_vars (l, r) = vars l \<union> vars r"
-
-adhoc_overloading
-  vars rule_vars
-
-value [nbe] "vars (Var 1, Var 0)"
-
-definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
-  "trs_vars R = \<Union>(rule_vars ` R)"
-
-adhoc_overloading
-  vars trs_vars
-
-value [nbe] "vars {(Var 1, Var 0)}"
-
-text \<open>Sometimes it is necessary to add explicit type constraints
-before a variant can be determined.\<close>
-(*value "vars R" (*has multiple instances*)*)
-value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)"
-
-text \<open>It is also possible to remove variants.\<close>
-no_adhoc_overloading
-  vars term_vars rule_vars 
-
-(*value "vars (Var 1)" (*does not have an instance*)*)
-
-text \<open>As stated earlier, the overloaded constant is only used for
-input and output. Internally, always a variant is used, as can be
-observed by the configuration option \<open>show_variants\<close>.\<close>
-
-adhoc_overloading
-  vars term_vars
-
-declare [[show_variants]]
-
-term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*)
-
-
-subsection \<open>Adhoc Overloading inside Locales\<close>
-
-text \<open>As example we use permutations that are parametrized over an
-atom type \<^typ>\<open>'a\<close>.\<close>
-
-definition perms :: "('a \<Rightarrow> 'a) set" where
-  "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
-
-typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
-  by standard (auto simp: perms_def)
-
-text \<open>First we need some auxiliary lemmas.\<close>
-lemma permsI [Pure.intro]:
-  assumes "bij f" and "MOST x. f x = x"
-  shows "f \<in> perms"
-  using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg)
-
-lemma perms_imp_bij:
-  "f \<in> perms \<Longrightarrow> bij f"
-  by (simp add: perms_def)
-
-lemma perms_imp_MOST_eq:
-  "f \<in> perms \<Longrightarrow> MOST x. f x = x"
-  by (simp add: perms_def) (metis MOST_iff_finiteNeg)
-
-lemma id_perms [simp]:
-  "id \<in> perms"
-  "(\<lambda>x. x) \<in> perms"
-  by (auto simp: perms_def bij_def)
-
-lemma perms_comp [simp]:
-  assumes f: "f \<in> perms" and g: "g \<in> perms"
-  shows "(f \<circ> g) \<in> perms"
-  apply (intro permsI bij_comp)
-  apply (rule perms_imp_bij [OF g])
-  apply (rule perms_imp_bij [OF f])
-  apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]])
-  apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]])
-  by simp
-
-lemma perms_inv:
-  assumes f: "f \<in> perms"
-  shows "inv f \<in> perms"
-  apply (rule permsI)
-  apply (rule bij_imp_bij_inv)
-  apply (rule perms_imp_bij [OF f])
-  apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]])
-  apply (erule subst, rule inv_f_f)
-  apply (rule bij_is_inj [OF perms_imp_bij [OF f]])
-  done
-
-lemma bij_Rep_perm: "bij (Rep_perm p)"
-  using Rep_perm [of p] unfolding perms_def by simp
-
-instantiation perm :: (type) group_add
-begin
-
-definition "0 = Abs_perm id"
-definition "- p = Abs_perm (inv (Rep_perm p))"
-definition "p + q = Abs_perm (Rep_perm p \<circ> Rep_perm q)"
-definition "(p1::'a perm) - p2 = p1 + - p2"
-
-lemma Rep_perm_0: "Rep_perm 0 = id"
-  unfolding zero_perm_def by (simp add: Abs_perm_inverse)
-
-lemma Rep_perm_add:
-  "Rep_perm (p1 + p2) = Rep_perm p1 \<circ> Rep_perm p2"
-  unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm)
-
-lemma Rep_perm_uminus:
-  "Rep_perm (- p) = inv (Rep_perm p)"
-  unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)
-
-instance
-  apply standard
-  unfolding Rep_perm_inject [symmetric]
-  unfolding minus_perm_def
-  unfolding Rep_perm_add
-  unfolding Rep_perm_uminus
-  unfolding Rep_perm_0
-  apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
-  done
-
-end
-
-lemmas Rep_perm_simps =
-  Rep_perm_0
-  Rep_perm_add
-  Rep_perm_uminus
-
-
-section \<open>Permutation Types\<close>
-
-text \<open>We want to be able to apply permutations to arbitrary types. To
-this end we introduce a constant \<open>PERMUTE\<close> together with
-convenient infix syntax.\<close>
-
-consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "\<bullet>" 75)
-
-text \<open>Then we add a locale for types \<^typ>\<open>'b\<close> that support
-appliciation of permutations.\<close>
-locale permute =
-  fixes permute :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
-  assumes permute_zero [simp]: "permute 0 x = x"
-    and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)"
-begin
-
-adhoc_overloading
-  PERMUTE permute
-
-end
-
-text \<open>Permuting atoms.\<close>
-definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "permute_atom p a = (Rep_perm p) a"
-
-adhoc_overloading
-  PERMUTE permute_atom
-
-interpretation atom_permute: permute permute_atom
-  by standard (simp_all add: permute_atom_def Rep_perm_simps)
-
-text \<open>Permuting permutations.\<close>
-definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
-  "permute_perm p q = p + q - p"
-
-adhoc_overloading
-  PERMUTE permute_perm
-
-interpretation perm_permute: permute permute_perm
-  apply standard
-  unfolding permute_perm_def
-  apply simp
-  apply (simp only: diff_conv_add_uminus minus_add add.assoc)
-  done
-
-text \<open>Permuting functions.\<close>
-locale fun_permute =
-  dom: permute perm1 + ran: permute perm2
-  for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
-  and perm2 :: "'a perm \<Rightarrow> 'c \<Rightarrow> 'c"
-begin
-
-adhoc_overloading
-  PERMUTE perm1 perm2
-
-definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where
-  "permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))"
-
-adhoc_overloading
-  PERMUTE permute_fun
-
-end
-
-sublocale fun_permute \<subseteq> permute permute_fun
-  by (unfold_locales, auto simp: permute_fun_def)
-     (metis dom.permute_plus minus_add)
-
-lemma "(Abs_perm id :: nat perm) \<bullet> Suc 0 = Suc 0"
-  unfolding permute_atom_def
-  by (metis Rep_perm_0 id_apply zero_perm_def)
-
-interpretation atom_fun_permute: fun_permute permute_atom permute_atom
-  by (unfold_locales)
-
-adhoc_overloading
-  PERMUTE atom_fun_permute.permute_fun
-
-lemma "(Abs_perm id :: 'a perm) \<bullet> id = id"
-  unfolding atom_fun_permute.permute_fun_def
-  unfolding permute_atom_def
-  by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def)
-
-end
-
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/ex/Coherent.thy
--- a/src/HOL/ex/Coherent.thy	Mon Jul 13 15:23:32 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-(*  Title:      HOL/ex/Coherent.thy
-    Author:     Stefan Berghofer, TU Muenchen
-    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
-*)
-
-section \<open>Coherent Logic Problems\<close>
-
-theory Coherent
-imports Main
-begin
-
-subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
-
-no_notation
-  comp (infixl "o" 55) and
-  relcomp (infixr "O" 75)
-
-lemma p1p2:
-  assumes "col a b c l \<and> col d e f m"
-    and "col b f g n \<and> col c e g o"
-    and "col b d h p \<and> col a e h q"
-    and "col c d i r \<and> col a f i s"
-    and "el n o \<Longrightarrow> goal"
-    and "el p q \<Longrightarrow> goal"
-    and "el s r \<Longrightarrow> goal"
-    and "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
-    and "\<And>A B. pl A B \<Longrightarrow> ep A A"
-    and "\<And>A B. ep A B \<Longrightarrow> ep B A"
-    and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
-    and "\<And>A B. pl A B \<Longrightarrow> el B B"
-    and "\<And>A B. el A B \<Longrightarrow> el B A"
-    and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
-    and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
-    and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
-    and "\<And>A B C D E F G H I J K L M N O P Q.
-           col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
-           col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
-           (\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> pl G D"
-    and "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C"
-    and "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
-  shows goal using assms
-  by coherent
-
-lemma p2p1:
-  assumes "col a b c l \<and> col d e f m"
-    and "col b f g n \<and> col c e g o"
-    and "col b d h p \<and> col a e h q"
-    and "col c d i r \<and> col a f i s"
-    and "pl a m \<Longrightarrow> goal"
-    and "pl b m \<Longrightarrow> goal"
-    and "pl c m \<Longrightarrow> goal"
-    and "pl d l \<Longrightarrow> goal"
-    and "pl e l \<Longrightarrow> goal"
-    and "pl f l \<Longrightarrow> goal"
-    and "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
-    and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
-    and "\<And>A B. pl A B \<Longrightarrow> ep A A"
-    and "\<And>A B. ep A B \<Longrightarrow> ep B A"
-    and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
-    and "\<And>A B. pl A B \<Longrightarrow> el B B"
-    and "\<And>A B. el A B \<Longrightarrow> el B A"
-    and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
-    and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
-    and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
-    and "\<And>A B C D E F G H I J K L M N O P Q.
-           col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
-           col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
-           (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
-    and "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B"
-    and "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
-  shows goal using assms
-  by coherent
-
-
-subsection \<open>Preservation of the Diamond Property under reflexive closure\<close>
-
-lemma diamond:
-  assumes "reflexive_rewrite a b" "reflexive_rewrite a c"
-    and "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
-    and "\<And>A. equalish A A" 
-    and "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
-    and "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
-    and "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
-    and "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
-    and "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
-    and "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
-  shows goal using assms
-  by coherent
-
-end
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/ex/Commands.thy
--- a/src/HOL/ex/Commands.thy	Mon Jul 13 15:23:32 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,77 +0,0 @@
-(*  Title:      HOL/ex/Commands.thy
-    Author:     Makarius
-*)
-
-section \<open>Some Isar command definitions\<close>
-
-theory Commands
-imports Main
-keywords
-  "print_test" :: diag and
-  "global_test" :: thy_decl and
-  "local_test" :: thy_decl
-begin
-
-subsection \<open>Diagnostic command: no state change\<close>
-
-ML \<open>
-  Outer_Syntax.command \<^command_keyword>\<open>print_test\<close> "print term test"
-    (Parse.term >> (fn s => Toplevel.keep (fn st =>
-      let
-        val ctxt = Toplevel.context_of st;
-        val t = Syntax.read_term ctxt s;
-        val ctxt' = Proof_Context.augment t ctxt;
-      in Pretty.writeln (Syntax.pretty_term ctxt' t) end)));
-\<close>
-
-print_test x
-print_test "\<lambda>x. x = a"
-
-
-subsection \<open>Old-style global theory declaration\<close>
-
-ML \<open>
-  Outer_Syntax.command \<^command_keyword>\<open>global_test\<close> "test constant declaration"
-    (Parse.binding >> (fn b => Toplevel.theory (fn thy =>
-      let
-        val thy' = Sign.add_consts [(b, \<^typ>\<open>'a\<close>, NoSyn)] thy;
-      in thy' end)));
-\<close>
-
-global_test a
-global_test b
-print_test a
-
-
-subsection \<open>Local theory specification\<close>
-
-ML \<open>
-  Outer_Syntax.local_theory \<^command_keyword>\<open>local_test\<close> "test local definition"
-    (Parse.binding -- (\<^keyword>\<open>=\<close> |-- Parse.term) >> (fn (b, s) => fn lthy =>
-      let
-        val t = Syntax.read_term lthy s;
-        val (def, lthy') = Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), t)) lthy;
-      in lthy' end));
-\<close>
-
-local_test true = True
-print_test true
-thm true_def
-
-local_test identity = "\<lambda>x. x"
-print_test "identity x"
-thm identity_def
-
-context fixes x y :: nat
-begin
-
-local_test test = "x + y"
-print_test test
-thm test_def
-
-end
-
-print_test "test 0 1"
-thm test_def
-
-end
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/ex/Groebner_Examples.thy
--- a/src/HOL/ex/Groebner_Examples.thy	Mon Jul 13 15:23:32 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,116 +0,0 @@
-(*  Title:      HOL/ex/Groebner_Examples.thy
-    Author:     Amine Chaieb, TU Muenchen
-*)
-
-section \<open>Groebner Basis Examples\<close>
-
-theory Groebner_Examples
-imports Main
-begin
-
-subsection \<open>Basic examples\<close>
-
-lemma
-  fixes x :: int
-  shows "x ^ 3 = x ^ 3"
-  apply (tactic \<open>ALLGOALS (CONVERSION
-    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
-  by (rule refl)
-
-lemma
-  fixes x :: int
-  shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<^sup>2 + (80 * x + 32))))" 
-  apply (tactic \<open>ALLGOALS (CONVERSION
-    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
-  by (rule refl)
-
-schematic_goal
-  fixes x :: int
-  shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X" 
-  apply (tactic \<open>ALLGOALS (CONVERSION
-    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv \<^context>))))\<close>)
-  by (rule refl)
-
-lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{comm_ring_1})"
-  apply (simp only: power_Suc power_0)
-  apply (simp only: semiring_norm)
-  oops
-
-lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"
-  by algebra
-
-lemma "(4::nat) + 4 = 3 + 5"
-  by algebra
-
-lemma "(4::int) + 0 = 4"
-  apply algebra?
-  by simp
-
-lemma
-  assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0"
-  shows "d\<^sup>2 * c\<^sup>2 - 2 * d * c * a * f + a\<^sup>2 * f\<^sup>2 - e * d * b * c - e * b * a * f +
-    a * e\<^sup>2 * c + f * d * b\<^sup>2 = 0"
-  using assms by algebra
-
-lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"
-  by algebra
-
-theorem "x* (x\<^sup>2 - x  - 5) - 3 = (0::int) \<longleftrightarrow> (x = 3 \<or> x = -1)"
-  by algebra
-
-lemma
-  fixes x::"'a::idom"
-  shows "x\<^sup>2*y = x\<^sup>2 & x*y\<^sup>2 = y\<^sup>2 \<longleftrightarrow>  x = 1 & y = 1 | x = 0 & y = 0"
-  by algebra
-
-subsection \<open>Lemmas for Lagrange's theorem\<close>
-
-definition
-  sq :: "'a::times => 'a" where
-  "sq x == x*x"
-
-lemma
-  fixes x1 :: "'a::{idom}"
-  shows
-  "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
-    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
-    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
-    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
-    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
-  by (algebra add: sq_def)
-
-lemma
-  fixes p1 :: "'a::{idom}"
-  shows
-  "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
-   (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
-    = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
-      sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
-      sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
-      sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
-      sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
-      sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
-      sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
-      sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
-  by (algebra add: sq_def)
-
-
-subsection \<open>Colinearity is invariant by rotation\<close>
-
-type_synonym point = "int \<times> int"
-
-definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
-  "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).
-    ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))"
-
-lemma collinear_inv_rotation:
-  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
-  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
-    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
-  using assms 
-  by (algebra add: collinear_def split_def fst_conv snd_conv)
-
-lemma "\<exists>(d::int). a*y - a*x = n*d \<Longrightarrow> \<exists>u v. a*u + n*v = 1 \<Longrightarrow> \<exists>e. y - x = n*e"
-  by algebra
-
-end
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/ex/Induction_Schema.thy
--- a/src/HOL/ex/Induction_Schema.thy	Mon Jul 13 15:23:32 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(*  Title:      HOL/ex/Induction_Schema.thy
-    Author:     Alexander Krauss, TU Muenchen
-*)
-
-section \<open>Examples of automatically derived induction rules\<close>
-
-theory Induction_Schema
-imports Main
-begin
-
-subsection \<open>Some simple induction principles on nat\<close>
-
-lemma nat_standard_induct: (* cf. Nat.thy *)
-  "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
-by induction_schema (pat_completeness, lexicographic_order)
-
-lemma nat_induct2:
-  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
-  \<Longrightarrow> P n"
-by induction_schema (pat_completeness, lexicographic_order)
-
-lemma minus_one_induct:
-  "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x"
-by induction_schema (pat_completeness, lexicographic_order)
-
-theorem diff_induct: (* cf. Nat.thy *)
-  "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
-    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
-by induction_schema (pat_completeness, lexicographic_order)
-
-lemma list_induct2': (* cf. List.thy *)
-  "\<lbrakk> P [] [];
-  \<And>x xs. P (x#xs) [];
-  \<And>y ys. P [] (y#ys);
-   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
- \<Longrightarrow> P xs ys"
-by induction_schema (pat_completeness, lexicographic_order)
-
-theorem even_odd_induct:
-  assumes "R 0"
-  assumes "Q 0"
-  assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)"
-  assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)"
-  shows "R n" "Q n"
-  using assms
-by induction_schema (pat_completeness+, lexicographic_order)
-
-end
diff -r 08f1e4cb735f -r c6756adfef0f src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Mon Jul 13 15:23:32 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,344 +0,0 @@
-(*  Title:      HOL/ex/Records.thy
-    Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel,
-                TU Muenchen
-*)
-
-section \<open>Using extensible records in HOL -- points and coloured points\<close>
-
-theory Records
-imports Main
-begin
-
-subsection \<open>Points\<close>
-
-record point =
-  xpos :: nat
-  ypos :: nat
-
-text \<open>
-  Apart many other things, above record declaration produces the
-  following theorems:
-\<close>
-
-
-thm point.simps
-thm point.iffs
-thm point.defs
-
-text \<open>
-  The set of theorems @{thm [source] point.simps} is added
-  automatically to the standard simpset, @{thm [source] point.iffs} is
-  added to the Classical Reasoner and Simplifier context.
-
-  \medskip Record declarations define new types and type abbreviations:
-  @{text [display]
-\<open>point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
-'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type\<close>}
-\<close>
-
-consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
-consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)"
-
-
-subsubsection \<open>Introducing concrete records and record schemes\<close>
-
-definition foo1 :: point
-  where "foo1 = (| xpos = 1, ypos = 0 |)"
-
-definition foo3 :: "'a => 'a point_scheme"
-  where "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)"
-
-
-subsubsection \<open>Record selection and record update\<close>
-
-definition getX :: "'a point_scheme => nat"
-  where "getX r = xpos r"
-
-definition setX :: "'a point_scheme => nat => 'a point_scheme"
-  where "setX r n = r (| xpos := n |)"
-
-
-subsubsection \<open>Some lemmas about records\<close>
-
-text \<open>Basic simplifications.\<close>
-
-lemma "point.make n p = (| xpos = n, ypos = p |)"
-  by (simp only: point.make_def)
-
-lemma "xpos (| xpos = m, ypos = n, ... = p |) = m"
-  by simp
-
-lemma "(| xpos = m, ypos = n, ... = p |) (| xpos:= 0 |) = (| xpos = 0, ypos = n, ... = p |)"
-  by simp
-
-
-text \<open>\medskip Equality of records.\<close>
-
-lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)"
-  \<comment> \<open>introduction of concrete record equality\<close>
-  by simp
-
-lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'"
-  \<comment> \<open>elimination of concrete record equality\<close>
-  by simp
-
-lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
-  \<comment> \<open>introduction of abstract record equality\<close>
-  by simp
-
-lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'"
-  \<comment> \<open>elimination of abstract record equality (manual proof)\<close>
-proof -
-  assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs")
-  then have "xpos ?lhs = xpos ?rhs" by simp
-  then show ?thesis by simp
-qed
-
-
-text \<open>\medskip Surjective pairing\<close>
-
-lemma "r = (| xpos = xpos r, ypos = ypos r |)"
-  by simp
-
-lemma "r = (| xpos = xpos r, ypos = ypos r, ... = point.more r |)"
-  by simp
-
-
-text \<open>
-  \medskip Representation of records by cases or (degenerate)
-  induction.
-\<close>
-
-lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
-proof (cases r)
-  fix xpos ypos more
-  assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
-  then show ?thesis by simp
-qed
-
-lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
-proof (induct r)
-  fix xpos ypos more
-  show "(| xpos = xpos, ypos = ypos, ... = more |) (| xpos := n, ypos := m |) =
-      (| xpos = xpos, ypos = ypos, ... = more |) (| ypos := m, xpos := n |)"
-    by simp
-qed
-
-lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
-proof (cases r)
-  fix xpos ypos more
-  assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>"
-  then show ?thesis by simp
-qed
-
-lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
-proof (cases r)
-  case fields
-  then show ?thesis by simp
-qed
-
-lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
-  by (cases r) simp
-
-
-text \<open>
- \medskip Concrete records are type instances of record schemes.
-\<close>
-
-definition foo5 :: nat
-  where "foo5 = getX (| xpos = 1, ypos = 0 |)"
-
-
-text \<open>\medskip Manipulating the ``\<open>...\<close>'' (more) part.\<close>
-
-definition incX :: "'a point_scheme => 'a point_scheme"
-  where "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
-
-lemma "incX r = setX r (Suc (getX r))"
-  by (simp add: getX_def setX_def incX_def)
-
-
-text \<open>An alternative definition.\<close>
-
-definition incX' :: "'a point_scheme => 'a point_scheme"
-  where "incX' r = r (| xpos := xpos r + 1 |)"
-
-
-subsection \<open>Coloured points: record extension\<close>
-
-datatype colour = Red | Green | Blue
-
-record cpoint = point +
-  colour :: colour
-
-
-text \<open>
-  The record declaration defines a new type constructor and abbreviations:
-  @{text [display]
-\<open>cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) =
-  () cpoint_ext_type point_ext_type
-'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) =
-  'a cpoint_ext_type point_ext_type\<close>}
-\<close>
-
-consts foo6 :: cpoint
-consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)"
-consts foo8 :: "'a cpoint_scheme"
-consts foo9 :: "(| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"
-
-
-text \<open>
- Functions on \<open>point\<close> schemes work for \<open>cpoints\<close> as well.
-\<close>
-
-definition foo10 :: nat
-  where "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
-
-
-subsubsection \<open>Non-coercive structural subtyping\<close>
-
-text \<open>
- Term \<^term>\<open>foo11\<close> has type \<^typ>\<open>cpoint\<close>, not type \<^typ>\<open>point\<close> ---
- Great!
-\<close>
-
-definition foo11 :: cpoint
-  where "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
-
-
-subsection \<open>Other features\<close>
-
-text \<open>Field names contribute to record identity.\<close>
-
-record point' =
-  xpos' :: nat
-  ypos' :: nat
-
-text \<open>
-  \noindent May not apply \<^term>\<open>getX\<close> to @{term [source] "(| xpos' =
-  2, ypos' = 0 |)"} -- type error.
-\<close>
-
-text \<open>\medskip Polymorphic records.\<close>
-
-record 'a point'' = point +
-  content :: 'a
-
-type_synonym cpoint'' = "colour point''"
-
-
-
-text \<open>Updating a record field with an identical value is simplified.\<close>
-lemma "r (| xpos := xpos r |) = r"
-  by simp
-
-text \<open>Only the most recent update to a component survives simplification.\<close>
-lemma "r (| xpos := x, ypos := y, xpos := x' |) = r (| ypos := y, xpos := x' |)"
-  by simp
-
-text \<open>In some cases its convenient to automatically split
-(quantified) records. For this purpose there is the simproc @{ML [source]
-"Record.split_simproc"} and the tactic @{ML [source]
-"Record.split_simp_tac"}.  The simplification procedure
-only splits the records, whereas the tactic also simplifies the
-resulting goal with the standard record simplification rules. A
-(generalized) predicate on the record is passed as parameter that
-decides whether or how `deep' to split the record. It can peek on the
-subterm starting at the quantified occurrence of the record (including
-the quantifier). The value \<^ML>\<open>0\<close> indicates no split, a value
-greater \<^ML>\<open>0\<close> splits up to the given bound of record extension and
-finally the value \<^ML>\<open>~1\<close> completely splits the record.
-@{ML [source] "Record.split_simp_tac"} additionally takes a list of
-equations for simplification and can also split fixed record variables.
-
-\<close>
-
-lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
-  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
-  apply simp
-  done
-
-lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
-  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
-  apply simp
-  done
-
-lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
-  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
-  apply simp
-  done
-
-lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
-  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
-  apply simp
-  done
-
-lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
-  apply auto
-  done
-
-lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
-  apply auto
-  done
-
-lemma "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
-  apply auto
-  done
-
-lemma True
-proof -
-  {
-    fix P r
-    assume pre: "P (xpos r)"
-    then have "\<exists>x. P x"
-      apply -
-      apply (tactic \<open>Record.split_simp_tac \<^context> [] (K ~1) 1\<close>)
-      apply auto
-      done
-  }
-  show ?thesis ..
-qed
-
-text \<open>The effect of simproc @{ML [source] Record.ex_sel_eq_simproc} is
-  illustrated by the following lemma.\<close>
-
-lemma "\<exists>r. xpos r = x"
-  apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>)
-  done
-
-
-subsection \<open>A more complex record expression\<close>
-
-record ('a, 'b, 'c) bar = bar1 :: 'a
-  bar2 :: 'b
-  bar3 :: 'c
-  bar21 :: "'b \<times> 'a"
-  bar32 :: "'c \<times> 'b"
-  bar31 :: "'c \<times> 'a"
-
-print_record "('a,'b,'c) bar"
-
-subsection \<open>Some code generation\<close>
-
-export_code foo1 foo3 foo5 foo10 checking SML
-
-text \<open>
-  Code generation can also be switched off, for instance for very large records
-\<close>
-
-declare [[record_codegen = false]]
-
-record not_so_large_record =
-  bar520 :: nat
-  bar521 :: "nat * nat"
-
-declare [[record_codegen = true]]
-
-end
diff -r 08f1e4cb735f -r c6756adfef0f src/Pure/Admin/build_cygwin.scala
--- a/src/Pure/Admin/build_cygwin.scala	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Pure/Admin/build_cygwin.scala	Wed Jul 15 16:28:26 2020 +0200
@@ -42,7 +42,7 @@
           progress.bash(
             File.bash_path(cygwin_exe) + " --site " + Bash.string(mirror) + " --no-verify" +
               " --local-package-dir 'C:\\temp'" +
-              " --root " + Bash.string(File.platform_path(cygwin)) +
+              " --root " + File.bash_platform_path(cygwin) +
               " --packages " + quote((packages ::: more_packages).mkString(",")) +
               " --no-shortcuts --no-startmenu --no-desktop --quiet-mode",
             echo = true)
diff -r 08f1e4cb735f -r c6756adfef0f src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Pure/Concurrent/future.ML	Wed Jul 15 16:28:26 2020 +0200
@@ -176,22 +176,21 @@
 fun report_status () = (*requires SYNCHRONIZED*)
   if ! ML_statistics then
     let
-      val {ready, pending, running, passive, urgent, total} = Task_Queue.status (! queue);
+      val {ready, pending, running, passive, urgent} = Task_Queue.status (! queue);
       val workers_total = length (! workers);
       val workers_active = count_workers Working;
       val workers_waiting = count_workers Waiting;
-      val stats =
-       [("now", Value.print_real (Time.toReal (Time.now ()))),
-        ("tasks_ready", Value.print_int ready),
-        ("tasks_pending", Value.print_int pending),
-        ("tasks_running", Value.print_int running),
-        ("tasks_passive", Value.print_int passive),
-        ("tasks_urgent", Value.print_int urgent),
-        ("tasks_total", Value.print_int total),
-        ("workers_total", Value.print_int workers_total),
-        ("workers_active", Value.print_int workers_active),
-        ("workers_waiting", Value.print_int workers_waiting)] @
-        ML_Statistics.get ();
+      val _ =
+        ML_Statistics.set
+         {tasks_ready = ready,
+          tasks_pending = pending,
+          tasks_running = running,
+          tasks_passive = passive,
+          tasks_urgent = urgent,
+          workers_total = workers_total,
+          workers_active = workers_active,
+          workers_waiting = workers_waiting};
+      val stats = ML_Statistics.get ();
     in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end
   else ();
 
diff -r 08f1e4cb735f -r c6756adfef0f src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Jul 15 16:28:26 2020 +0200
@@ -34,8 +34,7 @@
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val total_jobs: queue -> int
-  val status: queue ->
-    {ready: int, pending: int, running: int, passive: int, urgent: int, total: int}
+  val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
   val cancel: queue -> group -> Thread.thread list
   val cancel_all: queue -> group list * Thread.thread list
   val finish: task -> queue -> bool * queue
@@ -278,7 +277,7 @@
 
 (* queue status *)
 
-fun status (Queue {jobs, urgent, total, ...}) =
+fun status (Queue {jobs, urgent, ...}) =
   let
     val (x, y, z, w) =
       Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
@@ -287,7 +286,7 @@
           | Running _ => (x, y, z + 1, w)
           | Passive _ => (x, y, z, w + 1)))
         jobs (0, 0, 0, 0);
-  in {ready = x, pending = y, running = z, passive = w, urgent = urgent, total = total} end;
+  in {ready = x, pending = y, running = z, passive = w, urgent = urgent} end;
 
 
 
diff -r 08f1e4cb735f -r c6756adfef0f src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Pure/General/file.scala	Wed Jul 15 16:28:26 2020 +0200
@@ -124,6 +124,8 @@
   def bash_path(path: Path): String = Bash.string(standard_path(path))
   def bash_path(file: JFile): String = Bash.string(standard_path(file))
 
+  def bash_platform_path(path: Path): String = Bash.string(platform_path(path))
+
 
   /* directory entries */
 
diff -r 08f1e4cb735f -r c6756adfef0f src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Pure/ML/ml_statistics.ML	Wed Jul 15 16:28:26 2020 +0200
@@ -6,64 +6,133 @@
 
 signature ML_STATISTICS =
 sig
-  val get: unit -> Properties.T
+  val set: {tasks_ready: int, tasks_pending: int, tasks_running: int, tasks_passive: int,
+    tasks_urgent: int, workers_total: int, workers_active: int, workers_waiting: int} -> unit
+  val get: unit -> (string * string) list
+  val get_external: int -> (string * string) list
+  val monitor: int -> real -> unit
 end;
 
 structure ML_Statistics: ML_STATISTICS =
 struct
 
-fun get () =
-  let
-    val
-     {gcFullGCs,
-      gcPartialGCs,
-      gcSharePasses,
-      sizeAllocation,
-      sizeAllocationFree,
-      sizeCode,
-      sizeHeap,
-      sizeHeapFreeLastFullGC,
-      sizeHeapFreeLastGC,
-      sizeStacks,
-      threadsInML,
-      threadsTotal,
-      threadsWaitCondVar,
-      threadsWaitIO,
-      threadsWaitMutex,
-      threadsWaitSignal,
-      timeGCReal,
-      timeGCSystem,
-      timeGCUser,
-      timeNonGCReal,
-      timeNonGCSystem,
-      timeNonGCUser,
-      userCounters} = PolyML.Statistics.getLocalStats ();
-    val user_counters =
-      Vector.foldri
-        (fn (i, j, res) => ("user_counter" ^ Value.print_int i, Value.print_int j) :: res)
-        [] userCounters;
-  in
-    [("full_GCs", Value.print_int gcFullGCs),
-     ("partial_GCs", Value.print_int gcPartialGCs),
-     ("share_passes", Value.print_int gcSharePasses),
-     ("size_allocation", Value.print_int sizeAllocation),
-     ("size_allocation_free", Value.print_int sizeAllocationFree),
-     ("size_code", Value.print_int sizeCode),
-     ("size_heap", Value.print_int sizeHeap),
-     ("size_heap_free_last_full_GC", Value.print_int sizeHeapFreeLastFullGC),
-     ("size_heap_free_last_GC", Value.print_int sizeHeapFreeLastGC),
-     ("size_stacks", Value.print_int sizeStacks),
-     ("threads_in_ML", Value.print_int threadsInML),
-     ("threads_total", Value.print_int threadsTotal),
-     ("threads_wait_condvar", Value.print_int threadsWaitCondVar),
-     ("threads_wait_IO", Value.print_int threadsWaitIO),
-     ("threads_wait_mutex", Value.print_int threadsWaitMutex),
-     ("threads_wait_signal", Value.print_int threadsWaitSignal),
-     ("time_elapsed", Value.print_real (Time.toReal timeNonGCReal)),
-     ("time_elapsed_GC", Value.print_real (Time.toReal timeGCReal)),
-     ("time_CPU", Value.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
-     ("time_GC", Value.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
-    user_counters
+(* print *)
+
+fun print_int x = if x < 0 then "-" ^ Int.toString (~ x) else Int.toString x;
+
+fun print_real0 x =
+  let val s = Real.fmt (StringCvt.GEN NONE) x in
+    (case String.fields (fn c => c = #".") s of
+      [a, b] => if List.all (fn c => c = #"0") (String.explode b) then a else s
+    | _ => s)
   end;
 
+fun print_real x =
+  if x < 0.0 then "-" ^ print_real0 (~ x) else print_real0 x;
+
+val print_properties =
+  String.concatWith "," o map (fn (a, b) => a ^ "=" ^ b);
+
+
+(* set user properties *)
+
+fun set {tasks_ready, tasks_pending, tasks_running, tasks_passive, tasks_urgent,
+    workers_total, workers_active, workers_waiting} =
+ (PolyML.Statistics.setUserCounter (0, tasks_ready);
+  PolyML.Statistics.setUserCounter (1, tasks_pending);
+  PolyML.Statistics.setUserCounter (2, tasks_running);
+  PolyML.Statistics.setUserCounter (3, tasks_passive);
+  PolyML.Statistics.setUserCounter (4, tasks_urgent);
+  PolyML.Statistics.setUserCounter (5, workers_total);
+  PolyML.Statistics.setUserCounter (6, workers_active);
+  PolyML.Statistics.setUserCounter (7, workers_waiting));
+
+
+(* get properties *)
+
+fun make_properties
+   {gcFullGCs,
+    gcPartialGCs,
+    gcSharePasses,
+    sizeAllocation,
+    sizeAllocationFree,
+    sizeCode,
+    sizeHeap,
+    sizeHeapFreeLastFullGC,
+    sizeHeapFreeLastGC,
+    sizeStacks,
+    threadsInML,
+    threadsTotal,
+    threadsWaitCondVar,
+    threadsWaitIO,
+    threadsWaitMutex,
+    threadsWaitSignal,
+    timeGCReal,
+    timeGCSystem,
+    timeGCUser,
+    timeNonGCReal,
+    timeNonGCSystem,
+    timeNonGCUser,
+    userCounters} =
+  let
+    val tasks_ready = Vector.sub (userCounters, 0);
+    val tasks_pending = Vector.sub (userCounters, 1);
+    val tasks_running = Vector.sub (userCounters, 2);
+    val tasks_passive = Vector.sub (userCounters, 3);
+    val tasks_urgent = Vector.sub (userCounters, 4);
+    val tasks_total = tasks_ready + tasks_pending + tasks_running + tasks_passive + tasks_urgent;
+    val workers_total = Vector.sub (userCounters, 5);
+    val workers_active = Vector.sub (userCounters, 6);
+    val workers_waiting = Vector.sub (userCounters, 7);
+  in
+    [("now", print_real (Time.toReal (Time.now ()))),
+     ("tasks_ready", print_int tasks_ready),
+     ("tasks_pending", print_int tasks_pending),
+     ("tasks_running", print_int tasks_running),
+     ("tasks_passive", print_int tasks_passive),
+     ("tasks_urgent", print_int tasks_urgent),
+     ("tasks_total", print_int tasks_total),
+     ("workers_total", print_int workers_total),
+     ("workers_active", print_int workers_active),
+     ("workers_waiting", print_int workers_waiting),
+     ("full_GCs", print_int gcFullGCs),
+     ("partial_GCs", print_int gcPartialGCs),
+     ("share_passes", print_int gcSharePasses),
+     ("size_allocation", print_int sizeAllocation),
+     ("size_allocation_free", print_int sizeAllocationFree),
+     ("size_code", print_int sizeCode),
+     ("size_heap", print_int sizeHeap),
+     ("size_heap_free_last_full_GC", print_int sizeHeapFreeLastFullGC),
+     ("size_heap_free_last_GC", print_int sizeHeapFreeLastGC),
+     ("size_stacks", print_int sizeStacks),
+     ("threads_in_ML", print_int threadsInML),
+     ("threads_total", print_int threadsTotal),
+     ("threads_wait_condvar", print_int threadsWaitCondVar),
+     ("threads_wait_IO", print_int threadsWaitIO),
+     ("threads_wait_mutex", print_int threadsWaitMutex),
+     ("threads_wait_signal", print_int threadsWaitSignal),
+     ("time_elapsed", print_real (Time.toReal timeNonGCReal)),
+     ("time_elapsed_GC", print_real (Time.toReal timeGCReal)),
+     ("time_CPU", print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
+     ("time_GC", print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))]
+  end;
+
+fun get () =
+  make_properties (PolyML.Statistics.getLocalStats ());
+
+fun get_external pid =
+  make_properties (PolyML.Statistics.getRemoteStats pid);
+
+
+(* monitor process *)
+
+fun monitor pid delay =
+  let
+    fun loop () =
+      (TextIO.output (TextIO.stdOut, print_properties (get_external pid) ^ "\n");
+       TextIO.flushOut TextIO.stdOut;
+       OS.Process.sleep (Time.fromReal delay);
+       loop ());
+  in loop () handle Interrupt => OS.Process.exit OS.Process.success end;
+
 end;
diff -r 08f1e4cb735f -r c6756adfef0f src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Pure/ML/ml_statistics.scala	Wed Jul 15 16:28:26 2020 +0200
@@ -25,6 +25,31 @@
   def now(props: Properties.T): Double = Now.unapply(props).get
 
 
+  /* monitor process */
+
+  def monitor(pid: Long,
+    delay: Time = Time.seconds(0.5),
+    consume: Properties.T => Unit = Console.println)
+  {
+    def progress_stdout(line: String)
+    {
+      val props =
+        Library.space_explode(',', line).flatMap((entry: String) =>
+          Library.space_explode('=', entry) match {
+            case List(a, b) => Some((a, b))
+            case _ => None
+          })
+      if (props.nonEmpty) consume(props)
+    }
+
+    Bash.process("exec \"$POLYML_EXE\" -q --use " +
+      File.bash_platform_path(Path.explode("~~/src/Pure/ML/ml_statistics.ML")) +
+      " --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
+          ML_Syntax.print_double(delay.seconds)))
+      .result(progress_stdout = progress_stdout, strict = false).check
+  }
+
+
   /* memory fields (mega bytes) */
 
   def mem_print(x: Long): Option[String] =
diff -r 08f1e4cb735f -r c6756adfef0f src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Pure/ML/ml_syntax.scala	Wed Jul 15 16:28:26 2020 +0200
@@ -9,13 +9,14 @@
 
 object ML_Syntax
 {
-  /* int */
+  /* numbers */
 
-  private def signed_int(s: String): String =
+  private def signed(s: String): String =
     if (s(0) == '-') "~" + s.substring(1) else s
 
-  def print_int(i: Int): String = signed_int(Value.Int(i))
-  def print_long(i: Long): String = signed_int(Value.Long(i))
+  def print_int(x: Int): String = signed(Value.Int(x))
+  def print_long(x: Long): String = signed(Value.Long(x))
+  def print_double(x: Double): String = signed(Value.Double(x))
 
 
   /* string */
diff -r 08f1e4cb735f -r c6756adfef0f src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Pure/ROOT.ML	Wed Jul 15 16:28:26 2020 +0200
@@ -114,8 +114,6 @@
 ML_file "ML/exn_properties.ML";
 ML_file_no_debug "ML/exn_debugger.ML";
 
-ML_file "ML/ml_statistics.ML";
-
 ML_file "Concurrent/thread_data_virtual.ML";
 ML_file "Concurrent/isabelle_thread.ML";
 ML_file "Concurrent/single_assignment.ML";
diff -r 08f1e4cb735f -r c6756adfef0f src/Pure/ROOT0.ML
--- a/src/Pure/ROOT0.ML	Mon Jul 13 15:23:32 2020 +0000
+++ b/src/Pure/ROOT0.ML	Wed Jul 15 16:28:26 2020 +0200
@@ -1,5 +1,7 @@
 (*** Isabelle/Pure bootstrap: initial setup ***)
 
+ML_file "ML/ml_statistics.ML";
+
 ML_file "General/exn.ML";
 ML_file "General/output_primitives.ML";