src/Pure/Isar/calculation.ML
changeset 14282 b23f028c1651
parent 13371 82a057cf4413
child 14549 ea6e18e5c7a9
equal deleted inserted replaced
14281:a8c4a1e63071 14282:b23f028c1651
   140 
   140 
   141 fun maintain_calculation false calc state =
   141 fun maintain_calculation false calc state =
   142       state
   142       state
   143       |> put_calculation calc
   143       |> put_calculation calc
   144       |> Proof.simple_have_thms calculationN calc
   144       |> Proof.simple_have_thms calculationN calc
   145       |> Proof.reset_facts
       
   146   | maintain_calculation true calc state =
   145   | maintain_calculation true calc state =
   147       state
   146       state
   148       |> reset_calculation
   147       |> reset_calculation
   149       |> Proof.reset_thms calculationN
   148       |> Proof.reset_thms calculationN
   150       |> Proof.simple_have_thms "" calc
   149       |> Proof.simple_have_thms "" calc