src/HOL/Metis_Examples/Binary_Tree.thy
changeset 58889 5b7a9633cfa8
parent 58310 91ea607a34d8
child 63167 0909deb8059b
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     3     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     4 
     5 Metis example featuring binary trees.
     5 Metis example featuring binary trees.
     6 *)
     6 *)
     7 
     7 
     8 header {* Metis Example Featuring Binary Trees *}
     8 section {* Metis Example Featuring Binary Trees *}
     9 
     9 
    10 theory Binary_Tree
    10 theory Binary_Tree
    11 imports Main
    11 imports Main
    12 begin
    12 begin
    13 
    13