Theory ML_Unification.ML_Tactic_Utils

✐‹creator "Kevin Kappelmann"›
section ‹ML Tactic Utils›
theory ML_Tactic_Utils
  imports
    ML_Logger
    ML_Term_Utils
    ML_Conversion_Utils
    ML_Unification_Base
begin

paragraph ‹Summary›
text ‹Utilities for tactics.›

ML_file‹tactic_util.ML›
ML‹
(*Isabelle's default ORELSE in tactical.ML is not lazy; we patch this behaviour here.*)
(*TODO: should this be changed in tactical.ML itself?*)
val (op ORELSE) : tactic * tactic -> tactic = Tactic_Util.ORELSE
val (op ORELSE') : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic = Tactic_Util.ORELSE'
val TRY : tactic -> tactic = Tactic_Util.TRY
val FIRST : tactic list -> tactic = Tactic_Util.FIRST
val FIRST' : ('a -> tactic) list -> 'a -> tactic = Tactic_Util.FIRST'
›

end