src/Pure/defs.ML
changeset 17670 bf4f2c1b26cc
parent 17669 94dbbffbf94b
child 17707 bc0270e9d27f
equal deleted inserted replaced
17669:94dbbffbf94b 17670:bf4f2c1b26cc
     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