Merge branch 'main' into isabelle_nightly

This reverts commit e12abadc94.

.woodpecker/build.yml

@@ -1,6 +1,6 @@
 pipeline:
   build:
-    image: git.logicalhacking.com/lh-docker/lh-docker-isabelle/isabelle2023:latest
+    image: git.logicalhacking.com/lh-docker/lh-docker-isabelle/isabelle_nightly:latest
     pull: true
     commands:
       - hg log --limit 2 /root/isabelle
@@ -23,7 +23,7 @@ pipeline:
       - cd ../..
       - ln -s * latest
   archive:
-    image: git.logicalhacking.com/lh-docker/lh-docker-isabelle/isabelle2023:latest
+    image: git.logicalhacking.com/lh-docker/lh-docker-isabelle/isabelle_nightly:latest
     commands:
       - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
       - mkdir -p $ARTIFACT_DIR

Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy

@@ -544,7 +544,7 @@ text*[T4::technical]\<open>
 \<^enum>  \<^ML>\<open>Sign.typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv\<close>
 \<^enum>  \<^ML>\<open>Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int\<close>
 \<^enum>  \<^ML>\<open>Sign.const_type: theory -> string -> typ option\<close>
-\<^enum>  \<^ML>\<open>Sign.certify_term: theory -> term -> term * typ * int\<close>, the function for CERTIFICATION of types
+\<^enum>  \<^ML>\<open>Sign.certify_term: theory -> term -> term * typ\<close>, the function for CERTIFICATION of types
 \<^enum>  \<^ML>\<open>Sign.cert_term: theory -> term -> term\<close>, short-cut for the latter
 \<^enum>  \<^ML>\<open>Sign.tsig_of: theory -> Type.tsig\<close>, projects from a theory the type signature 
 \<close>
@@ -610,8 +610,6 @@ text\<open>Now we turn to the crucial issue of type-instantiation and with a giv
 subsection\<open>More operations on types\<close>
 
 text\<open>
-\<^item> \<^ML>\<open>Term_Subst.map_types_same : (typ -> typ) -> term -> term\<close>
-\<^item> \<^ML>\<open>Term_Subst.map_aterms_same : (term -> term) -> term -> term\<close>
 \<^item> \<^ML>\<open>Term_Subst.instantiate: typ TVars.table * term Vars.table -> term -> term\<close>
 \<^item> \<^ML>\<open>Term_Subst.instantiateT: typ TVars.table -> typ -> typ\<close>
 \<^item> \<^ML>\<open>Term_Subst.generalizeT: Names.set -> int -> typ -> typ\<close>
@@ -639,16 +637,13 @@ val ty' = Term_Subst.instantiateT S'' t_schematic;
 (* Don't know how to build a typ TVars.table *)
 val t = (generalize_term @{term "[]"});
 
-val t' = Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S')) (t)
+val t' = Term.map_types (Term_Subst.instantiateT S'') (t)
-(* or alternatively : *)
-val t'' = Term.map_types (Term_Subst.instantiateT S'') (t)
 \<close>
 
 text\<open>A more abstract env for variable management in tactic proofs. A bit difficult to use
   outside the very closed-up tracks of conventional use...\<close>
 
-ML\<open> Consts.the_const; (* T is a kind of signature ... *)
+ML\<open> Variable.import_terms;
-    Variable.import_terms;
     Vartab.update;\<close>
 
 subsection*[t232::technical]\<open> Type-Inference (= inferring consistent type information if possible) \<close>
@@ -903,7 +898,7 @@ With the exception of the \<^ML>\<open>Specification.axiomatization\<close> cons
 are all-together built as composition of conservative extensions.
 
 The components are a bit scattered in the architecture. A relatively recent and
-high-level component (more low-level components such as \<^ML>\<open>Global_Theory.add_defs\<close>
+high-level component (more low-level components such as \<^ML>\<open>Global_Theory.add_def\<close>
 exist) for definitions and axiomatizations is here:
 \<close>
 

Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy

@@ -1310,7 +1310,7 @@ ML
 \<open> DOF_core.get_onto_class_name_global "requirement" @{theory};
   Syntax.parse_typ                 @{context} "requirement";
   val Type(t,_) = Syntax.parse_typ @{context} "requirement" handle ERROR _ => dummyT; 
-  Syntax.read_typ                  @{context} "hypothesis"  handle  _ => dummyT;
+  Syntax.read_typ                  @{context} "hypothesis"  handle  ERROR _ => dummyT;
   Proof_Context.init_global; \<close>
 
 end

Isabelle_DOF/scala/dof.scala

@@ -39,10 +39,10 @@ import isabelle._
 object DOF {
   /** parameters **/
 
-  val isabelle_version = "2023"
+  val isabelle_version = ""
-  val isabelle_url = "https://isabelle.in.tum.de/website-Isabelle2023" 
+  val isabelle_url = "https://isabelle.sketis.net/devel/release_snapshot/"
 
-  val afp_version = "afp-2023-09-13"
+  val afp_version = "afp-devel"
 
   // Isabelle/DOF version: "Unreleased" for development, semantic version for releases
   val version = "Unreleased"

Isabelle_DOF/thys/Isa_DOF.thy

@@ -1866,7 +1866,7 @@ fun check_invariants thy binding =
 fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} binding cid_pos doc_attrs thy =
   let
     val oid = Binding.name_of binding
-    val (((name, args_cid), typ), pos') = check_classref is_monitor cid_pos thy
+    val (((name, args_cid), typ:typ), pos') = check_classref is_monitor cid_pos thy
     val cid_pos' = (name, pos')
     val cid_long = fst cid_pos'
     val default_cid = args_cid = DOF_core.default_cid
@@ -1891,13 +1891,13 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} bi
                             val defaults_init = create_default_object thy binding cid_long typ
                             fun conv (na, _(*ty*), parsed_term) =(Binding.name_of na, Binding.pos_of na, "=", parsed_term);
                             val S = map conv (DOF_core.get_attribute_defaults cid_long thy);
-                            val (defaults, _(*ty*), _) = calc_update_term {mk_elaboration=false}
+                            val (defaults, _) = calc_update_term {mk_elaboration=false}
                                                                       thy (name, typ) S defaults_init;
-                            val (value_term', _(*ty*), _) = calc_update_term {mk_elaboration=true}
+                            val (value_term', _) = calc_update_term {mk_elaboration=true}
                                                                       thy (name, typ) assns' defaults
                           in if Config.get_global thy DOF_core.object_value_debug
                              then let
-                                    val (input_term, _(*ty*), _) = calc_update_term {mk_elaboration=false}
+                                    val (input_term, _) = calc_update_term {mk_elaboration=false}
                                                                         thy (name, typ)  assns' defaults
                                   in (input_term, value_term') end
                              else (\<^term>\<open>()\<close>, value_term') end
@@ -2248,7 +2248,7 @@ fun meta_args_2_latex thy sem_attrs transform_attr
         fun ltx_of_markup ctxt s = let
   	                            val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s
                                 val str_of_term = ltx_of_term  ctxt true term 
-                                    handle _ => "Exception in ltx_of_term"
+                                  (*  handle _ => "Exception in ltx_of_term" *)
                               in
                                 str_of_term
                               end 

README.md

@@ -7,7 +7,7 @@ Isabelle/DOF allows for both conventional typesetting and formal development.
 
 Isabelle/DOF has two major prerequisites:
 
-* **Isabelle 2023:** Isabelle/DOF requires [Isabelle](https://isabelle.in.tum.de/)
+* **Isabelle (Development Version):** Isabelle/DOF requires [Isabelle](https://isabelle.in.tum.de/)
   and several entries from the [Archive of Formal Proofs
   (AFP)](https://www.isa-afp.org/).
 * **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least

README_DEVELOPMENT.md

@@ -5,9 +5,9 @@
 Isabelle/DOF has three major prerequisites:
 
 * **Isabelle:** Isabelle/DOF requires [Isabelle
-  2023](https://isabelle.in.tum.de/website-Isabelle2023/). Please download the
+  2022](https://isabelle.in.tum.de/website-Isabelle2022/). Please download the
-  Isabelle 2023 distribution for your operating system from the [Isabelle
+  Isabelle 2022 distribution for your operating system from the [Isabelle
-  website](https://isabelle.in.tum.de/website-Isabelle2023/).
+  website](https://isabelle.in.tum.de/website-Isabelle2022/).
 * **AFP:** Isabelle/DOF requires several entries from the [Archive of Formal Proofs
   (AFP)](https://www.isa-afp.org/).  
 * **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least