(* Title: HOL/Induct/Infinitely_Branching_Tree.thy Author: Stefan Berghofer, TU Muenchen Author: Lawrence C Paulson, Cambridge University Computer Laboratory *) section ‹Infinitely branching trees› theory Infinitely_Branching_Tree imports Main begin