doc-src/Tutorial/Datatype/autotac.ML
changeset 5851 15ce4c1c8313
equal deleted inserted replaced
5850:9712294e60b9 5851:15ce4c1c8313
       
     1 by(Auto_tac);