src/Pure/sign.ML
changeset 15723 5b594d6ec919
parent 15703 727ef1b8b3ee
child 15746 44260d72de35
equal deleted inserted replaced
15722:e40cd03ca048 15723:5b594d6ec919
  1271     |> add_path "/";
  1271     |> add_path "/";
  1272 
  1272 
  1273 end;
  1273 end;
  1274 
  1274 
  1275 end;
  1275 end;
       
  1276