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?
This way, please.

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, definition, primrec, inductive, apply, done are without quotation marks, as are the names of constants in constant definitions (consts and constdefs)
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 =.
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 Proof General 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 of a specific number type. Try e.g. "(1::nat) + 1 = 2" instead.
Can Isabelle/HOL find counterexamples?

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

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 Proof General 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: 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 have a predefined meaning in Isabelle, though).

System

I want to generate one of those flashy LaTeX documents. How?
You will need to work with the isabelle command in a Unix shell. The easiest way to get to a document is the following: use isabelle 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 isabelle 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 isabelle usedir -b HOL My_Image in that directory to create an image My_Image using the parent logic HOL. You should then be able to invoke Isabelle with isabelle emacs -l My_Image and have everything that is loaded in ROOT.ML instantly available.