# HG changeset patch # User wenzelm # Date 1491336454 -7200 # Node ID 9d9e6dac9690e90623bd6098ce2c0c43b9efd0ff # Parent ae93953746fca8872296ef5005a82906ace2c953 eliminated redundant imports; diff -r ae93953746fc -r 9d9e6dac9690 src/HOL/ROOT --- a/src/HOL/ROOT Tue Apr 04 21:57:43 2017 +0200 +++ b/src/HOL/ROOT Tue Apr 04 22:07:34 2017 +0200 @@ -216,11 +216,7 @@ "~~/src/HOL/Algebra/Ring" "~~/src/HOL/Algebra/FiniteProduct" theories - Pocklington - Gauss Number_Theory - Euclidean_Algorithm - Factorial_Ring document_files "root.tex" @@ -1039,7 +1035,6 @@ "~~/src/HOL/Library/Nat_Bijection" "~~/src/HOL/Library/Countable" theories - Fixrec HOLCF document_files "root.tex"