Is HORN-SAT in LIN, if so why is that not an indication that P=LIN? The Complexity Zoo defines $LIN$ to be the class of decision problems solvable by a deterministic Turing machine in linear time.

$$LIN \subseteq P$$

Since HORN-SAT is solvable in $O(n)$ (as indicated in Linear-time algorithms for testing the satisfiability of propositional horn formulae (1984)) 


  New algorithms for deciding whether a (propositional) Horn formula is satisfiable are presented. If the Horn formula $A$ contains $K$ distinct propositional letters and if it is assumed that they are exactly $P_1,…, P_K$, the two algorithms presented in this paper run in time $O(N)$, where $N$ is the total number of occurrences of literals in $A$. 


I am wondering why we can't conclude that

$$LIN = P$$

given that HORN-SAT has also been proven to be $P$-complete under log-space reduction? I must be missing something. Or is that a well-known fact?

(I have yet thoroughly gone through the 1984 paper so I don't quite understand the algorithms for solving HORN-SAT in linear time, and thus I may have misunderstood the implication.)
The deterministic time hierarchy theorem precludes all problems in P being decided in linear time.  If you try to reduce a problem to HORN-SAT that requires more than linear time to decide, you'll find that the reduction itself requires more than linear time.