src/Pure/Isar/proof.ML
changeset 6030 f29d4e507564
parent 6001 28b0a9891852
child 6091 e3cdbd929a24
equal deleted inserted replaced
6029:30c957a74803 6030:f29d4e507564
    98 (* type mode *)
    98 (* type mode *)
    99 
    99 
   100 datatype mode = Forward | ForwardChain | Backward;
   100 datatype mode = Forward | ForwardChain | Backward;
   101 
   101 
   102 val mode_name =
   102 val mode_name =
   103   fn Forward => "forward" | ForwardChain => "forward chain" | Backward => "backward";
   103   fn Forward => "state" | ForwardChain => "chain" | Backward => "prove";
   104 
   104 
   105 
   105 
   106 (* type node *)
   106 (* type node *)
   107 
   107 
   108 type node =
   108 type node =