src/Pure/Isar/method.ML
changeset 7504 0fec51813079
parent 7439 a1b3310b4985
child 7506 08a88d4ebd54
equal deleted inserted replaced
7503:e8be98558eb8 7504:0fec51813079
   345 fun tac text state =
   345 fun tac text state =
   346   state
   346   state
   347   |> Proof.goal_facts (K [])
   347   |> Proof.goal_facts (K [])
   348   |> refine text;
   348   |> refine text;
   349 
   349 
   350 fun then_tac text state =
   350 val then_tac = refine;
   351   state
       
   352   |> Proof.goal_facts Proof.the_facts
       
   353   |> refine text;
       
   354 
   351 
   355 
   352 
   356 (* structured proof steps *)
   353 (* structured proof steps *)
   357 
   354 
   358 val default_text = named_method "default";
   355 val default_text = named_method "default";