doc-src/Tutorial/Datatype/triemain.ML
changeset 5851 15ce4c1c8313
equal deleted inserted replaced
5850:9712294e60b9 5851:15ce4c1c8313
       
     1 Goal "!t v bs. lookup (update t as v) bs = \
       
     2 \              (if as=bs then Some v else lookup t bs)";