summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 03 Oct 2018 20:55:59 +0200 | |

changeset 69115 | 919a1b23c192 |

parent 69114 | 163626ddaa19 |

child 69116 | cbcc43a00cff |

child 69117 | 3d3e87835ae8 |

tuned

--- a/src/HOL/Library/Tree.thy Wed Oct 03 13:20:05 2018 +0200 +++ b/src/HOL/Library/Tree.thy Wed Oct 03 20:55:59 2018 +0200 @@ -351,7 +351,7 @@ have "(2::nat) ^ height t \<le> 2 ^ height t'" proof - have "2 ^ height t = size1 t" - using True by (simp add: complete_iff_height size1_if_complete) + using True by (simp add: size1_if_complete) also have "\<dots> \<le> size1 t'" using assms(2) by(simp add: size1_size) also have "\<dots> \<le> 2 ^ height t'" by (rule size1_height) finally show ?thesis .