summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 |