--- a/thys/Re1.thy	Thu Feb 26 16:35:10 2015 +0000
+++ b/thys/Re1.thy	Wed Mar 04 19:34:47 2015 +0000
@@ -346,6 +346,7 @@
 apply metis
 apply(simp)
 (* ALT case *)
+thm mkeps.simps
 apply(simp)
 apply(erule disjE)
 apply(simp)
@@ -361,6 +362,7 @@
 apply(rotate_tac 4)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+thm mkeps_flat
 apply(simp add: mkeps_flat)
 apply(auto)[1]
 thm Prf_flat_L nullable_correctness
@@ -369,7 +371,7 @@
 apply(subst (asm) POSIX_def)
 apply(clarify)
 apply(drule_tac x="v2" in spec)
-by metis
+by simp
 
 
 section {* Derivatives *}
@@ -727,6 +729,7 @@
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
 (* EMPTY case *)
+apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
 (* CHAR case *)

Binary file thys/notes.pdf has changed

--- a/thys/notes.tex	Thu Feb 26 16:35:10 2015 +0000
+++ b/thys/notes.tex	Wed Mar 04 19:34:47 2015 +0000
@@ -1,6 +1,7 @@
 \documentclass[11pt]{article}
 \usepackage[left]{lineno}
 \usepackage{amsmath}
+\usepackage{stmaryrd}
 
 \begin{document}
 %%%\linenumbers
@@ -377,6 +378,67 @@
 
 \subsection*{Problems in the paper proof}
 
-I cannot verify 
+I cannot verify\ldots
+
+
+
+\newpage
+\section*{Isabelle Cheat-Sheet}
+ 
+\begin{itemize} 
+\item The main notion in Isabelle is a \emph{theorem}.
+      Definitions, inductive predicates and recursive
+      functions all have underlying theorems. If a definition
+      is called \texttt{foo}, then the theorem will be called
+      \texttt{foo\_def}. Take a recursive function, say
+      \texttt{bar}, it will have a theorem that is called
+      \texttt{bar.simps} and will be added to the simplifier.
+      That means the simplifier will automatically 
+      Inductive predicates called \texttt{baz} will be called
+      \texttt{baz.intros}. For inductive predicates, there are
+      also theorems \texttt{baz.induct} and
+      \texttt{baz.cases}.    
+
+\item A \emph{goal-state} consists of one or more subgoals. If
+      there are \texttt{No more subgoals!} then the theorem is
+      proved. Each subgoal is of the form
+  
+      \[
+      \llbracket \ldots{}premises\ldots \rrbracket \Longrightarrow 
+      conclusion
+      \]  
+  
+      \noindent 
+      where $premises$ and $conclusion$ are formulas of type 
+      \texttt{bool}.
+      
+\item There are three low-level methods for applying one or
+      more theorem to a subgoal, called \texttt{rule},
+      \texttt{drule} and \texttt{erule}. The first applies a 
+      theorem to a conclusion of a goal. For example
+      
+      \[\texttt{apply}(\texttt{rule}\;thm)
+      \]
+ 
+      If the conclusion is of the form $\_ \wedge \_$,
+      $\_ \longrightarrow \_$ and $\forall\,x. \_$ the
+      $thm$ is called
+      
+      \begin{center}
+      \begin{tabular}{lcl}
+      $\_ \wedge \_$          &  $\Rightarrow$ & $conjI$\\
+      $\_ \longrightarrow \_$ &  $\Rightarrow$ & $impI$\\
+      $\forall\,x.\_$        &  $\Rightarrow$ & $allI$
+      \end{tabular}
+      \end{center}
+       
+      Many of such rule are called intro-rules and end with 
+      an ``$I$'', or in case of inductive predicates $\_.intros$.
+      
+      
+       
+       
+\end{itemize}
+ 
 
 \end{document}