Adaptations for Isabelle2025

Author: simondfoster

Countable_Set_Extra.thy

@@ -87,13 +87,6 @@ lemma cset_CollectD: "(a :: 'a::countable) \<in>\<^sub>c {x. P x}\<^sub>c \<Long
 lemma cset_Collect_cong: "(\<And>x. P x = Q x) ==> {x. P x}\<^sub>c = {x. Q x}\<^sub>c"
   by simp
 
-text \<open> Avoid eta-contraction for robust pretty-printing. \<close>
-
-print_translation \<open>
- [Syntax_Trans.preserve_binder_abs_tr'
-   @{const_syntax cset_Collect} @{syntax_const "_cColl"}]
-\<close>
-
 lift_definition cset_set :: "'a list \<Rightarrow> 'a cset" is set
   using countable_finite by blast
 

Finite_Fun.thy

@@ -459,6 +459,4 @@ text \<open> Hide implementation details for finite functions \<close>
 lifting_update ffun.lifting
 lifting_forget ffun.lifting
 
-unbundle no_lattice_syntax
-
 end

Function_Toolkit.thy

@@ -58,17 +58,17 @@ consts
   disjoint :: "'f \<Rightarrow> bool"
 
 adhoc_overloading 
-  disjoint rel_disjoint and
-  disjoint pfun_disjoint and 
-  disjoint list_disjoint 
+  disjoint \<rightleftharpoons> rel_disjoint and
+  disjoint \<rightleftharpoons> pfun_disjoint and 
+  disjoint \<rightleftharpoons> list_disjoint 
 
 subsection \<open> Partitions \<close>
 
 consts partitions :: "'f \<Rightarrow> 'a set \<Rightarrow> bool" (infix "partitions" 65)
 
 adhoc_overloading
-  partitions rel_partitions and
-  partitions pfun_partitions and
-  partitions list_partitions
+  partitions \<rightleftharpoons> rel_partitions and
+  partitions \<rightleftharpoons> pfun_partitions and
+  partitions \<rightleftharpoons> list_partitions
 
 end

Overriding.thy

@@ -37,6 +37,4 @@ lemma override_compat_iff: "P ## Q \<Longrightarrow> (P \<oplus> Q) ## R \<longl
 
 end
 
-unbundle no_lattice_syntax
-
 end

Partial_Fun.thy

@@ -1439,6 +1439,4 @@ text \<open> Hide implementation details for partial functions \<close>
 lifting_update pfun.lifting
 lifting_forget pfun.lifting
 
-unbundle no_lattice_syntax
-
 end

Partial_Inj.thy

@@ -203,6 +203,4 @@ lemma pfun_of_pinj_of_alist [code]:
 
 declare pinj_of_alist.simps [simp del]
 
-unbundle no_lattice_syntax
-
 end

Relation_Toolkit.thy

@@ -48,11 +48,11 @@ hide_const (open) dom
 consts dom :: "'f \<Rightarrow> 'a set"
 
 adhoc_overloading
-  dom Map.dom and
-  dom Relation.Domain and
-  dom Partial_Fun.pdom and
-  dom Finite_Fun.fdom and
-  dom Partial_Inj.pidom
+  dom \<rightleftharpoons> Map.dom and
+  dom \<rightleftharpoons> Relation.Domain and
+  dom \<rightleftharpoons> Partial_Fun.pdom and
+  dom \<rightleftharpoons> Finite_Fun.fdom and
+  dom \<rightleftharpoons> Partial_Inj.pidom
 
 subsection \<open> Range \<close>
 
@@ -61,11 +61,11 @@ hide_const (open) ran
 consts ran :: "'f \<Rightarrow> 'a set"
 
 adhoc_overloading
-  ran Map.ran and
-  ran Relation.Range and
-  ran Partial_Fun.pran and
-  ran Finite_Fun.fran and
-  ran Partial_Inj.piran
+  ran \<rightleftharpoons> Map.ran and
+  ran \<rightleftharpoons> Relation.Range and
+  ran \<rightleftharpoons> Partial_Fun.pran and
+  ran \<rightleftharpoons> Finite_Fun.fran and
+  ran \<rightleftharpoons> Partial_Inj.piran
 
 subsection \<open> Identity relation \<close>
 
@@ -86,9 +86,9 @@ text \<open> Composition is probably the most difficult of the Z functions to im
 consts zcomp :: "'f \<Rightarrow> 'g \<Rightarrow> 'h" 
 
 adhoc_overloading
-  zcomp Fun.comp and
-  zcomp pfun_comp and
-  zcomp ffun_comp
+  zcomp \<rightleftharpoons> Fun.comp and
+  zcomp \<rightleftharpoons> pfun_comp and
+  zcomp \<rightleftharpoons> ffun_comp
 
 text \<open> Once we overload @{term Fun.comp}, we need to at least have output syntax set up. \<close>
 
@@ -109,10 +109,10 @@ consts dom_res :: "'a set \<Rightarrow> 'r \<Rightarrow> 'r" (infixr "\<Zdres>"
 abbreviation ndres (infixr "\<Zndres>" 85) where "ndres A P \<equiv> CONST dom_res (- A) P" 
 
 adhoc_overloading 
-  dom_res rel_domres
-  and dom_res pdom_res
-  and dom_res fdom_res
-  and dom_res pinj_dres
+  dom_res \<rightleftharpoons> rel_domres
+  and dom_res \<rightleftharpoons> pdom_res
+  and dom_res \<rightleftharpoons> fdom_res
+  and dom_res \<rightleftharpoons> pinj_dres
 
 syntax "_ndres" :: "logic \<Rightarrow> logic \<Rightarrow> logic" 
 translations "_ndres A P" == "CONST dom_res (- A) P"
@@ -124,10 +124,10 @@ consts ran_res :: "'r \<Rightarrow> 'a set \<Rightarrow> 'r" (infixl "\<Zrres>"
 abbreviation nrres (infixl "\<Znrres>" 86) where "nrres P A \<equiv> CONST ran_res P (- A)"
 
 adhoc_overloading 
-  ran_res rel_ranres
-  and ran_res pran_res
-  and ran_res fran_res
-  and ran_res pinj_rres
+  ran_res \<rightleftharpoons> rel_ranres
+  and ran_res \<rightleftharpoons> pran_res
+  and ran_res \<rightleftharpoons> fran_res
+  and ran_res \<rightleftharpoons> pinj_rres
 
 subsection \<open> Relational inversion \<close>
 

Sequence_Toolkit.thy

@@ -139,14 +139,14 @@ subsection \<open> Domain \<close>
 definition dom_seq :: "'a list \<Rightarrow> \<nat> set" where
 [simp]: "dom_seq xs = {0..<#xs}"
 
-adhoc_overloading dom dom_seq
+adhoc_overloading dom \<rightleftharpoons> dom_seq
 
 subsection \<open> Range \<close>
 
 definition ran_seq :: "'a list \<Rightarrow> 'a set" where
 [simp]: "ran_seq xs = set xs"
 
-adhoc_overloading ran ran_seq
+adhoc_overloading ran \<rightleftharpoons> ran_seq
 
 subsection \<open> Filter \<close>
 

Set_Toolkit.thy

@@ -1,7 +1,7 @@
 section \<open> Set Toolkit \<close>
 
 theory Set_Toolkit
-  imports "HOL-Library.Adhoc_Overloading" "HOL-Library.Multiset" "Relation_Lib"
+  imports "HOL-Library.Multiset" "Relation_Lib"
 begin
 
 text \<open> The majority of the Z set toolkit is implemented in the core libraries of HOL. We could

Tabulate_Command.thy

@@ -51,7 +51,7 @@ fun tabulate_cmd raw_t state =
     val t' = HOLogic.tupled_lambda xp t
     (* Close the term, apply the tabulate function, and evaluate *)
     val ts' = dest_list (Value_Command.value ctx (check_term ctx (const @{const_name "tabulate"} $ t')));
-    fun term_string t = YXML.content_of (symbolic_string_of (pretty_term ctx' t));
+    fun term_string t = XML.content_of (YXML.parse_body (symbolic_string_of (pretty_term ctx' t)));
     val heads = (map term_string (map Free (rev xs)) @ [term_string t])
     val rows = (map ((fn (x, y) => (map term_string (strip_tuple x) @ [term_string y])) o dest_prod) ts');
   in Pretty.writeln ((print_table heads rows)) end;