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

src/HOL/PreList.thy

changeset 8862 | 78643f8449c6 |

parent 8840 | 18b76c137c41 |

child 9066 | b1e874e38dab |

equal
deleted
inserted
replaced

8861:8341f24e09b5 | 8862:78643f8449c6 |
---|---|

6 A basis for building theory List on. Is defined separately to serve as a |
6 A basis for building theory List on. Is defined separately to serve as a |

7 basis for theory ToyList in the documentation. |
7 basis for theory ToyList in the documentation. |

8 *) |
8 *) |

9 |
9 |

10 theory PreList = |
10 theory PreList = |

11 Option + WF_Rel + NatBin + Recdef + Record + RelPow + Calculation + SVC_Oracle |
11 Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + |

12 files "Integ/NatSimprocs.ML": |
12 SVC_Oracle: |

13 |
13 |

14 end |
14 end |