equal
deleted
inserted
replaced
18 echo |
18 echo |
19 echo " Recursively find .ML files, converting legacy tactic scripts to" |
19 echo " Recursively find .ML files, converting legacy tactic scripts to" |
20 echo " Isabelle/Isar tactic emulation." |
20 echo " Isabelle/Isar tactic emulation." |
21 echo " Note: conversion is only approximated, based on some heuristics." |
21 echo " Note: conversion is only approximated, based on some heuristics." |
22 echo |
22 echo |
23 echo " Renames new versions of FILES by appending \".thy\"." |
23 echo " Renames old versions of FILES by appending \"~0~\"." |
|
24 echo " Creates new versions of FILES by appending \".thy\"." |
24 echo |
25 echo |
25 exit 1 |
26 exit 1 |
26 } |
27 } |
27 |
28 |
28 |
29 |