Top Level Strutcure
The top level is a theory structure. The name of the theory must match the file name. 

Definitions
This is the programlike. Similar to data and functions on that data. 
The keyword 'primrec' is used for a certain type of 'primative recursion' where each recursive call peels off a datatype constructor from one of the arguments.
Notation
 'a = type variable
Eamples of 'datatype'
 datatype bool = True  False
 datatype nat = 0  Suc nat
 datatype 'a list = Nil  Cons 'a " 'a list"
fun
fun defines a function by pattern matching over datatype constructors.
Examples of 'fun'
 fun conj :: "bool => bool => bool" where
"conj True True = True" 
"conj _ _ = False"  fun add :: "nat => nat => nat" where
"add 0 n = n" 
"add (Suc m) n = Suc (add m n)"
definiton
A definiton defines a nonrecursive function without any pattern matching
Examples of 'definiton'
 definition sq :: "nat => nat" where
"sq n = n n"
Abbreviations
Abbreviations have the same form as definitons but are only synthetic sugar.
Theorems, Lemmas and Rules
Theorems, Lemmas and Rules are the same to the program. The difference is only intended to express the importance. 
Proofs
We cannot prove all possible theorems but there are varying levels of search that we can use: 

 done tells Isabelle to associate the lemma just proved with its name
 thm name  displays the theorem
Examples of Proofs
 lemma add_02: "add m 0 =m"
apply (induction m)
apply(auto)
done
Results
The results show the proof state. The numbered lines are known as subgoals.
The prefix Vm: is Isabelle’s way of saying "for an arbitrary but fixed m". Universal quantifier at the meta level
The ==> separates assumptions from the conclusion.
Meta Level
/\ !!x. F 
Universal quantifier at the meta level Used to denote parameters F=another metalevel formula 
A ==> B  A ==> B ==> C A and B implies C A,B=other metalevel formula 
λ %x . F 
Lambda abstraction binds variables 
= 
Examples
This example creates a list structure 


This example proves theorems about 'or' 

Isar
proof ::= 'proof' method statement* 'qed'  'by' method statement ::= 'fix' variable+  'assume' proposition+  ('from' fact+)? 'have' proposition+ proof  ('from' fact+)? 'show' proposition+ proof proposition ::= (label':')? string fact ::= label method ::= ''  'this'  'rule' fact  'simp'  'blast'  'auto'  'induct' variable  ... 
 show statement establishes the conclusion of the proof
 have statement is for establishing intermediate results
shortcuts
 'this' refers to the fact proved by the previous statement.
 'then' = 'from this'
 'hence' = 'then have'
 'thus' = 'then show'
 'with' fact+ = 'from' fact+ 'and' 'this'
 '.' = 'by this'
 '..' = 'by' rule where Isabelle guesses the rule