equal
deleted
inserted
replaced
12 |
12 |
13 ( |
13 ( |
14 cat <<EOF |
14 cat <<EOF |
15 (* |
15 (* |
16 This file was generated by the "make_metis" script. The BSD License is used |
16 This file was generated by the "make_metis" script. The BSD License is used |
17 with Joe Hurd's kind permission. Extract from a September 13, 2010 email |
17 with Joe Leslie-Hurd's kind permission. Extract from a September 13, 2010 |
18 written by Joe Hurd: |
18 email written by him: |
19 |
19 |
20 I hereby give permission to the Isabelle team to release Metis as part |
20 I hereby give permission to the Isabelle team to release Metis as part |
21 of Isabelle, with the Metis code covered under the Isabelle BSD |
21 of Isabelle, with the Metis code covered under the Isabelle BSD |
22 license. |
22 license. |
23 *) |
23 *) |