src/HOL/NewNumberTheory/ROOT.ML
changeset 32805 9b535493ac8d
parent 32804 ca430e6aee1c
parent 32783 e43d761a742d
child 32806 06561afcadaa
child 32845 d2d0b9b1a69d
equal deleted inserted replaced
32804:ca430e6aee1c 32805:9b535493ac8d
     1 use_thys ["Fib","Residues"];