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

src/HOL/Data_Structures/Binomial_Heap.thy

changeset 72812 | caf2fd14e28b |

parent 72808 | ba65dc3e35af |

child 72910 | c145be662fbd |

equal
deleted
inserted
replaced

72809:64d8a7e6d8fa | 72812:caf2fd14e28b |
---|---|

6 |
6 |

7 theory Binomial_Heap |
7 theory Binomial_Heap |

8 imports |
8 imports |

9 "HOL-Library.Pattern_Aliases" |
9 "HOL-Library.Pattern_Aliases" |

10 Complex_Main |
10 Complex_Main |

11 "HOL-Data_Structures.Priority_Queue_Specs" |
11 Priority_Queue_Specs |

12 begin |
12 begin |

13 |
13 |

14 text \<open> |
14 text \<open> |

15 We formalize the binomial heap presentation from Okasaki's book. |
15 We formalize the binomial heap presentation from Okasaki's book. |

16 We show the functional correctness and complexity of all operations. |
16 We show the functional correctness and complexity of all operations. |