Session Stern_Brocot
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.BNF_Corec
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML›
Cotree
Cotree_Algebra
Stern_Brocot_Tree
Bird_Tree