What are the differences between LCF's Theorem and Automath's Prop?
The difference is in what kind of type theorem/Prop is.
In Isabelle, theorem is a type in the underlying implementation language, that is made abstract so that the only way to create an inhabitant of that type (i.e. a valid theorem) is in the end to resort to the primitives provided by the kernel. So it is the typing constraints of the implementation language together with the restricted primitives that forces you to inhabit only correct theorems. Also, in that setting proofs can be any program in the implementation language producing an object of type theorem, but they have no specific status, and cannot be manipulated directly.
On the contrary, Prop is a type in the theory of Coq, but not in its implementation language: if you look at the OCaml code, there is no such thing as a Prop type, only a type of terms. Verifying that a term (written in a specific language called Gallina, the proof/programming language of Coq) is indeed a valid proof is a job of a specific type-checker. This type-checker is the kernel. In that setting, proofs have a specific status, being syntactical objects of a given type of terms in the implementation, and as such can be manipulated, inspected and so on. In particular, the tactic languages are used to generate such proofs, which is not the same as directly constructing an inhabitant of theorem, because such terms will still in the end be inspected by the kernel, which is the only judge of what is a valid proof.