src/Provers/blast.ML
changeset 25365 4e7a1dabd7ef
parent 24112 6c4e7d17f9b0
child 26928 ca87aff1ad2d
equal deleted inserted replaced
25364:7f012f56efa3 25365:4e7a1dabd7ef
  1291      the resulting tactics, trace, etc.                            ***)
  1291      the resulting tactics, trace, etc.                            ***)
  1292 
  1292 
  1293 val fullTrace = ref ([]: branch list list);
  1293 val fullTrace = ref ([]: branch list list);
  1294 
  1294 
  1295 (*Read a string to make an initial, singleton branch*)
  1295 (*Read a string to make an initial, singleton branch*)
  1296 fun readGoal thy s = Sign.read_prop thy s |> fromTerm thy |> rand |> mkGoal;
  1296 fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
  1297 
  1297 
  1298 fun tryInThy thy lim s =
  1298 fun tryInThy thy lim s =
  1299   let
  1299   let
  1300     val state as State {fullTrace = ft, ...} = initialize thy;
  1300     val state as State {fullTrace = ft, ...} = initialize thy;
  1301     val res = timeap prove
  1301     val res = timeap prove