equal
deleted
inserted
replaced
6 there are no cyclic definitions. The algorithm is described in "An |
6 there are no cyclic definitions. The algorithm is described in "An |
7 Algorithm for Determining Definitional Cycles in Higher-Order Logic |
7 Algorithm for Determining Definitional Cycles in Higher-Order Logic |
8 with Overloading", Steven Obua, technical report, to be written :-) |
8 with Overloading", Steven Obua, technical report, to be written :-) |
9 |
9 |
10 ATTENTION: |
10 ATTENTION: |
11 Currently this implementation of the cylce test contains a bug of which the author is fully aware. |
11 Currently this implementation of the cycle test contains a bug of which the author is fully aware. |
12 This bug makes it possible to introduce inconsistent definitional cycles in Isabelle. |
12 This bug makes it possible to introduce inconsistent definitional cycles in Isabelle. |
13 *) |
13 *) |
14 |
14 |
15 signature DEFS = |
15 signature DEFS = |
16 sig |
16 sig |