# HG changeset patch
# User nipkow
# Date 1634065080 -7200
# Node ID 7422950f395551c1590eca5b424997cac0341bf0
# Parent  907483081d4c571ae755d62ecad7d0546159b90f# Parent  403ce50e6a2a31175ae8e21f6b02478e71983c28
merged

diff -r 403ce50e6a2a -r 7422950f3955 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue Oct 12 20:57:43 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Tue Oct 12 20:58:00 2021 +0200
@@ -183,7 +183,7 @@
 
 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
   e.g. from conj_forward, should have the form
-    "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
+    "\<lbrakk>P' \<Longrightarrow> ?P; Q' \<Longrightarrow> ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"
   and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
 fun forward_res ctxt nf st =
   let
@@ -293,7 +293,7 @@
   of SOME(th,_) => th
    | NONE => raise THM("forward_res2", 0, [st]);
 
-(*Remove duplicates in P|Q by assuming ~P in Q
+(*Remove duplicates in P\<or>Q by assuming \<not>P in Q
   rls (initially []) accumulates assumptions of the form P==>False*)
 fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc)
     handle THM _ => tryres(th,rls)
@@ -617,7 +617,7 @@
 
 val ext_cong_neq = @{thm ext_cong_neq}
 
-(* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
+(* Strengthens "f g \<noteq> f h" to "f g \<noteq> f h \<and> (\<exists>x. g x \<noteq> h x)". *)
 fun cong_extensionalize_thm ctxt th =
   (case Thm.concl_of th of
     \<^Const_>\<open>Trueprop for \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<close>\<close>\<close>\<close> =>
diff -r 403ce50e6a2a -r 7422950f3955 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 12 20:57:43 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 12 20:58:00 2021 +0200
@@ -71,10 +71,7 @@
             |> mk_old_skolem_term_wrapper
           val comb = list_comb (rhs, args)
         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
-      | dec_sko \<^Const_>\<open>All _ for \<open>Abs (a, T, p)\<close>\<close> rhss =
-        (*Universal quant: insert a free variable into body and continue*)
-        let val fname = singleton (Name.variant_list (Misc_Legacy.add_term_names (p, []))) a
-        in dec_sko (subst_bound (Free(fname,T), p)) rhss end
+      | dec_sko \<^Const_>\<open>All _ for \<open>Abs abs\<close>\<close> rhss = dec_sko (#2 (Term.dest_abs abs)) rhss
       | dec_sko \<^Const_>\<open>conj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko \<^Const_>\<open>disj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko \<^Const_>\<open>Trueprop for p\<close> rhss = dec_sko p rhss
@@ -183,7 +180,7 @@
 
 (* Given the definition of a Skolem function, return a theorem to replace
    an existential formula by a use of that function.
-   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
+   Example: "\<exists>x. x \<in> A \<and> x \<notin> B \<Longrightarrow> sko A B \<in> A \<and> sko A B \<notin> B" *)
 fun old_skolem_theorem_of_def ctxt rhs0 =
   let
     val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of ctxt