src/Pure/Isar/calculation.ML
changeset 6781 0db24da2a3c1
parent 6778 2f66eea8a025
child 6782 adf099e851ed
equal deleted inserted replaced
6780:769cea1985e4 6781:0db24da2a3c1
   133     calculations
   133     calculations
   134     |> Seq.map (fn calc =>
   134     |> Seq.map (fn calc =>
   135       (prt calc;
   135       (prt calc;
   136         state
   136         state
   137         |> Proof.bind_i [(Syntax.dddot_indexname, dddot)]
   137         |> Proof.bind_i [(Syntax.dddot_indexname, dddot)]
       
   138         |> put_calculation calc
   138         |> have_thm calc
   139         |> have_thm calc
   139         |> (if final then I else Proof.reset_facts)))
   140         |> (if final then Proof.chain else Proof.reset_facts)))
   140   end;
   141   end;
   141 
   142 
   142 val also = calculate false;
   143 fun also prt = calculate false prt;
   143 val finally = calculate true;
   144 fun finally prt = calculate true prt;
   144 
   145 
   145 
   146 
   146 
   147 
   147 (** theory setup **)
   148 (** theory setup **)
   148 
   149