equal
deleted
inserted
replaced
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 |