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

src/HOL/PreList.thy

changeset 21457 | 84a21cf15923 |

parent 21330 | 6dd5919e7742 |

child 22844 | 91c05f4b509e |

equal
deleted
inserted
replaced

21456:1c2b9df41e98 | 21457:84a21cf15923 |
---|---|

6 |
6 |

7 header {* A Basis for Building the Theory of Lists *} |
7 header {* A Basis for Building the Theory of Lists *} |

8 |
8 |

9 theory PreList |
9 theory PreList |

10 imports Wellfounded_Relations Presburger Relation_Power SAT |
10 imports Wellfounded_Relations Presburger Relation_Power SAT |

11 Hilbert_Choice FunDef Extraction |
11 FunDef Extraction |

12 begin |
12 begin |

13 |
13 |

14 text {* |
14 text {* |

15 This is defined separately to serve as a basis for |
15 This is defined separately to serve as a basis for |

16 theory ToyList in the documentation. |
16 theory ToyList in the documentation. |