What is the formal and complete definition of the words "meta-logic" and "object-logic" in Isabelle? I see people keep using these but could not find any definition for these.
You don't find them because they are specific to Isabelle (as far as I know). "Object-logic" and "meta-logic" are terms introduced by Larry Paulson (as far as I can tell). In general, though not specifically, they are related to the general terms "metalanguage" and "object language", for disciplines like logic and set theory. Do a search on those and you'll get the standard wiki pages, because they're a standard part of logic.
Here, I'm looking at page 16, 2.2.3 Meta and object language of Logic and Computation - Interactive Proof with Cambridge LCF, by Larry Paulson, published 1987. At that time he was still conforming to standard terms, but then he switched. I forgot where I read it, but he made the switch somewhere to "meta-logic" and "object-logic", to clarify things for his own purpose. The two terms are in his papers and in the Isabelle distribution docs.
Others can give you their expert knowledge, but the meta-logic specifically is what you get when you import the theory Pure, in particular, a minimal set of logical connectives, ==>, \<And>, &&&, and ==. Discussion of these are spread throughout the Isabelle distribution documentation.
I know nothing much about intuitionistic logic, other than it doesn't provide the law of excluded middle, but you will read that they provide a minimal, intuitionistic logic.
Don't thank me. I've just read some things here and there, and listened. Others can provide expert knowledge.