theory PresentationWeb
  imports Main

begin

notepad
begin
  fix A B 
  assume A and imp: "A \<Longrightarrow> B"
  term A            \<comment> \<open>A :: bool, object-logic (HOL) type\<close>
  term "A \<Longrightarrow> B"    \<comment> \<open>A \<Longrightarrow> B :: prop, meta-logic (Pure) type\<close>
  have B
    using imp[OF \<open>A\<close>].
end

end