General Questions

What is Isabelle?
Isabelle is a generic proof assistant developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).
Where can I find documentation?
This way, please.
Is it available for download?
Yes, it is available from several mirror sites, e. g. from Munich. It runs on common Unix systems (Linux, Mac OS X, BSD, Solaris, etc.).

Syntax

There are lots of arrows in Isabelle/HOL. What's the difference between ->, =>, -->, and ==> ?
Isabelle uses the => arrow for the function type (contrary to most functional languages which use ->). So a => b is the type of a function that takes an element of a as input and gives you an element of b as output. The long arrow --> and ==> are object and meta level implication. Roughly speaking, the meta level implication should be used to separate the assumptions from the conclusion in rule statements. Whenever you need an implication inside a closed HOL formula, use -->.
Where do I have to put those double quotes?
Isabelle distinguishes between inner and outer syntax. The outer syntax comes from the Isabelle framework, the inner syntax is the one in between quotation marks and comes from the object logic (in this case HOL). With time the distinction between the two becomes obvious, but in the beginning the following rules of thumb may work: types should be inside quotation marks, formulas and lemmas should be inside quotation marks, rules and equations (e.g. for definitions) should be inside quotation marks, commands like lemma, consts, primrec, constdefs, apply, done are without quotation marks, as are the names of constants in constant definitions (consts and constdefs)
What is No such constant: _case_syntax supposed to tell me?
You get this message if you use a case construct on a datatype and have a typo in the names of the constructor patterns or if the order of the constructors in the case pattern is different from the order in which they where defined (in the datatype definition).
Why doesn't Isabelle/HOL understand my equation?
Isabelle's equality = binds relatively strongly, so an equation like a = b & c might not be what you intend. Isabelle parses it as (a = b) & c. If you want it the other way around, you must set explicit parentheses as in a = (b & c). You may also consider to use the equivalence operator <-> which has lower precedence than =. This also applies to e.g. function definitions.
What does it mean not a proper equation?
Most commonly this is an instance of the question above. The primrec command (and others) expect equations as input, and since equality binds strongly in Isabelle/HOL, something like f x = b & c is not what you might expect it to be: Isabelle parses it as (f x = b) & c (which is indeed not a proper equation). To turn it into an equation you must set explicit parentheses: f x = (b & c), or sue the equivalence operator <-> instead: f x <-> (b &c)

Proving

What does empty result sequence mean?
It means that the applied proof method (or tactic) was unsuccessful. It did not transform the goal in any way, or simply just failed to do anything. You must try another tactic (or give the one you used more hints or lemmas to work with)
The Simplifier doesn't want to apply my rule, what's wrong?
Most commonly this is a typing problem. The rule you want to apply may require a more special (or just plain different) type from what you have in the current goal. Use the ProofGeneral menu Isabelle/Isar -> Settings -> Show Types and the thm command on the rule you want to apply to find out if the types are what you expect them to be (also take a look at the types in your goal). Show Sorts, Show Constants, and Trace Simplifier in the same menu may also be helpful.
If I do auto, it leaves me a goal False. Is my theorem wrong?
Not necessarily. It just means that auto transformed the goal into something that is not provable any more. That could be due to auto doing something stupid, or e.g. due to some earlier step in the proof that lost important information. It is of course also possible that the goal was never provable in the first place.
Why does lemma "1 + 1 = 2" fail?
Because it is not necessarily true. Isabelle/HOL does not assume that 1 and 2 are natural numbers. Try "(1::nat) + 1 = 2" instead.
Can Isabelle/HOL find counterexamples?

For arithmetic goals, arith finds counterexamples. For executable goals, quickcheck tries to find a counterexample. For goals of a more logical nature (including quantifiers, sets and inductive definitions) refute searches for a counter model.

Otherwise, negate the proposition and instantiate (some) variables with concrete values. You may also need additional assumptions about these values. For example, True & False ~= True | False is a counterexample of A & B = A | B, and A = ~B ==> A & B ~= A | B is another one. Sometimes Isabelle can help you to find the counterexample: just negate the proposition and do auto or simp. If lucky, you are left with the assumptions you need for the counterexample to work.

Sometimes when I enter a lemma proposition it takes a long time until proof mode is entered. What's the reason for this?
This is due to auto quickcheck: each toplevel goal entered in interactive mode is automatically checked for counterexamples. You can set a timeout for this feature or turn it off using the ProofGeneral menu Isabelle/Isar -> Settings.
Is there any chance to model generic monads and such?
Perhaps the AWE toolkit provides a solution for your problem.

Interface

X-Symbol doesn't seem to work. What can I do?
The most common reason why X-Symbol doesn't work is: it's not switched on yet. Assuming you are using ProofGeneral and have installed the X-Symbol package, you still need to turn X-Symbol on in ProofGeneral: select the menu items Proof-General -> Options -> X-Symbol and (if you want to save the setting for future sessions) select Options -> Save Options in XEmacs.
How do I input those X-Symbols anyway?
There are lots of ways to input x-symbols. The one that always works is writing it out in plain text (e.g. for the 'and' symbol type \<and>). For common symbols you can try to "paint them in ASCII" and if the X-Symbol package recognizes them it will automatically convert them into their graphical representation. Examples: --> is converted into the long single arrow, /\ is converted into the 'and' symbol, the sequence =_ into the equivalence sign, <_ into less-or-equal, [| into opening semantic brackets, and so on. For greek characters, the rotate command works well: to input α type a and then C-. (control and .). You can also display the grid-of-characters in the x-symbol menu to get an overview of the available graphical representations (not all of them already have a meaning in Isabelle, though).

System

I want to generate one of those flashy LaTeX documents. How?
You will need to work with the isatool command for this (in a Unix shell). The easiest way to get to a document is the following: use isatool mkdir to set up a new directory. The command will also create a file called IsaMakefile in the current directory. Put your theory file(s) into the new directory and edit the file ROOT.ML in there (following the comments) to tell Isabelle which of the theories to load (and in which order). Go back to the parent directory (where the IsaMakefile is) and type isatool make. Isabelle should then process your theories and tell you where to find the finished document. For more information on generating documents see the Isabelle Tutorial, Chapter 4.
I have a large formalization with many theories. Must I process all of them all of the time?
No, you can tell Isabelle to build a so-called heap image. This heap image can contain your pre-loaded theories. To get one, set up a directory with a ROOT.ML file (as for generating a document) and use the command isatool usedir -b HOL MyImage in that directory to create an image MyImage using the parent logic HOL. You should then be able to invoke Isabelle with Isabelle -l MyImage and have everything that is loaded in ROOT.ML instantly available.