equal
deleted
inserted
replaced
5 section \<open>2-3 Trees\<close> |
5 section \<open>2-3 Trees\<close> |
6 |
6 |
7 theory Tree23 |
7 theory Tree23 |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
|
10 |
|
11 hide_const (open) or |
10 |
12 |
11 text\<open>This is a very direct translation of some of the functions in table.ML |
13 text\<open>This is a very direct translation of some of the functions in table.ML |
12 in the Isabelle source code. That source is due to Makarius Wenzel and Stefan |
14 in the Isabelle source code. That source is due to Makarius Wenzel and Stefan |
13 Berghofer. |
15 Berghofer. |
14 |
16 |