--- a/src/HOL/Tools/try0.ML Thu Oct 24 16:45:09 2024 +0200
+++ b/src/HOL/Tools/try0.ML Thu Oct 24 16:46:25 2024 +0200
@@ -8,7 +8,7 @@
sig
val noneN : string
val silence_methods : bool -> Proof.context -> Proof.context
- datatype modifier = Simp | Intro | Elim | Dest
+ datatype modifier = Use | Simp | Intro | Elim | Dest
type result = {name: string, command: string, time: int, state: Proof.state}
val try0 : Time.time option -> ((Facts.ref * Token.src list) * modifier list) list ->
Proof.state -> result list
@@ -44,7 +44,7 @@
|> Scan.read Token.stopper Method.parse
|> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
-datatype modifier = Simp | Intro | Elim | Dest
+datatype modifier = Use | Simp | Intro | Elim | Dest
fun string_of_xthm (xref, args) =
Facts.string_of_ref xref ^