NEWS
changeset 72290 efb7fd4a6d1f
parent 72272 587d4681240c
child 72300 b17be02a0a11
equal deleted inserted replaced
72289:69880fdc8310 72290:efb7fd4a6d1f
   106 "supply subst_all [simp del] [[simproc del: defined_all]]"
   106 "supply subst_all [simp del] [[simproc del: defined_all]]"
   107 to leave fragile proofs unaffected.
   107 to leave fragile proofs unaffected.
   108 
   108 
   109 
   109 
   110 *** ML ***
   110 *** ML ***
       
   111 
       
   112 * Theory_Data extend operation is obsolete and needs to be the identity
       
   113 function; merge should be conservative and not reset to the empty value.
       
   114 Subtle INCOMPATIBILITY and change of semantics (due to
       
   115 Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
       
   116 the begin of a new theory can be achieved via Theory.at_begin.
   111 
   117 
   112 * Antiquotations @{scala_function} and @{scala} refer to registered
   118 * Antiquotations @{scala_function} and @{scala} refer to registered
   113 Isabelle/Scala functions (of type String => String): invocation works
   119 Isabelle/Scala functions (of type String => String): invocation works
   114 via the PIDE protocol.
   120 via the PIDE protocol.
   115 
   121