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

src/HOL/PreList.thy

changeset 10212 | 33fe2d701ddd |

parent 9619 | 6125cc9efc18 |

child 10261 | bb2f1e859177 |

equal
deleted
inserted
replaced

10211:1bece7f35762 | 10212:33fe2d701ddd |
---|---|

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 + NatSimprocs + Recdef + Record + RelPow + Calculation + |
11 Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + |

12 SVC_Oracle + While: |
12 Relation_Power + Calculation + SVC_Oracle + While: |

13 |
13 |

14 theorems [cases type: bool] = case_split |
14 theorems [cases type: bool] = case_split |

15 |
15 |

16 end |
16 end |