# HG changeset patch
# User Chengsong
# Date 1648292990 0
# Node ID e5dd8cc0aa82e594f93ab59d7bf2323638d44cd9
# Parent  a0f27e21b42cb818428c68d7632602c5908614b4
all electron pics removed

diff -r a0f27e21b42c -r e5dd8cc0aa82 ChengsongTanPhdThesis/Chapters/Chapter1.tex
--- a/ChengsongTanPhdThesis/Chapters/Chapter1.tex	Fri Mar 25 21:49:53 2022 +0000
+++ b/ChengsongTanPhdThesis/Chapters/Chapter1.tex	Sat Mar 26 11:09:50 2022 +0000
@@ -1547,42 +1547,42 @@
 \subsection{Figures}
 
 There will hopefully be many figures in your thesis (that should be placed in the \emph{Figures} folder). The way to insert figures into your thesis is to use a code template like this:
-\begin{verbatim}
-\begin{figure}
-\centering
-\includegraphics{Figures/Electron}
-\decoRule
-\caption[An Electron]{An electron (artist's impression).}
-\label{fig:Electron}
-\end{figure}
-\end{verbatim}
-Also look in the source file. Putting this code into the source file produces the picture of the electron that you can see in the figure below.
+%\begin{verbatim}
+%\begin{figure}
+%\centering
+%\includegraphics{Figures/Electron}
+%\decoRule
+%\caption[An Electron]{An electron (artist's impression).}
+%\label{fig:Electron}
+%\end{figure}
+%\end{verbatim}
+%Also look in the source file. Putting this code into the source file produces the picture of the electron that you can see in the figure below.
+%
+%\begin{figure}[th]
+%\centering
+%\includegraphics{Figures/Electron}
+%\decoRule
+%\caption[An Electron]{An electron (artist's impression).}
+%\label{fig:Electron}
+%\end{figure}
 
-\begin{figure}[th]
-\centering
-\includegraphics{Figures/Electron}
-\decoRule
-\caption[An Electron]{An electron (artist's impression).}
-\label{fig:Electron}
-\end{figure}
-
-Sometimes figures don't always appear where you write them in the source. The placement depends on how much space there is on the page for the figure. Sometimes there is not enough room to fit a figure directly where it should go (in relation to the text) and so \LaTeX{} puts it at the top of the next page. Positioning figures is the job of \LaTeX{} and so you should only worry about making them look good!
-
-Figures usually should have captions just in case you need to refer to them (such as in Figure~\ref{fig:Electron}). The \verb|\caption| command contains two parts, the first part, inside the square brackets is the title that will appear in the \emph{List of Figures}, and so should be short. The second part in the curly brackets should contain the longer and more descriptive caption text.
-
-The \verb|\decoRule| command is optional and simply puts an aesthetic horizontal line below the image. If you do this for one image, do it for all of them.
-
-\LaTeX{} is capable of using images in pdf, jpg and png format.
-
-\subsection{Typesetting mathematics}
-
-If your thesis is going to contain heavy mathematical content, be sure that \LaTeX{} will make it look beautiful, even though it won't be able to solve the equations for you.
-
-The \enquote{Not So Short Introduction to \LaTeX} (available on \href{http://www.ctan.org/tex-archive/info/lshort/english/lshort.pdf}{CTAN}) should tell you everything you need to know for most cases of typesetting mathematics. If you need more information, a much more thorough mathematical guide is available from the AMS called, \enquote{A Short Math Guide to \LaTeX} and can be downloaded from:
-\url{ftp://ftp.ams.org/pub/tex/doc/amsmath/short-math-guide.pdf}
-
-There are many different \LaTeX{} symbols to remember, luckily you can find the most common symbols in \href{http://ctan.org/pkg/comprehensive}{The Comprehensive \LaTeX~Symbol List}.
-
+%Sometimes figures don't always appear where you write them in the source. The placement depends on how much space there is on the page for the figure. Sometimes there is not enough room to fit a figure directly where it should go (in relation to the text) and so \LaTeX{} puts it at the top of the next page. Positioning figures is the job of \LaTeX{} and so you should only worry about making them look good!
+%
+%Figures usually should have captions just in case you need to refer to them (such as in Figure~\ref{fig:Electron}). The \verb|\caption| command contains two parts, the first part, inside the square brackets is the title that will appear in the \emph{List of Figures}, and so should be short. The second part in the curly brackets should contain the longer and more descriptive caption text.
+%
+%The \verb|\decoRule| command is optional and simply puts an aesthetic horizontal line below the image. If you do this for one image, do it for all of them.
+%
+%\LaTeX{} is capable of using images in pdf, jpg and png format.
+%
+%\subsection{Typesetting mathematics}
+%
+%If your thesis is going to contain heavy mathematical content, be sure that \LaTeX{} will make it look beautiful, even though it won't be able to solve the equations for you.
+%
+%The \enquote{Not So Short Introduction to \LaTeX} (available on \href{http://www.ctan.org/tex-archive/info/lshort/english/lshort.pdf}{CTAN}) should tell you everything you need to know for most cases of typesetting mathematics. If you need more information, a much more thorough mathematical guide is available from the AMS called, \enquote{A Short Math Guide to \LaTeX} and can be downloaded from:
+%\url{ftp://ftp.ams.org/pub/tex/doc/amsmath/short-math-guide.pdf}
+%
+%There are many different \LaTeX{} symbols to remember, luckily you can find the most common symbols in \href{http://ctan.org/pkg/comprehensive}{The Comprehensive \LaTeX~Symbol List}.
+%
 You can write an equation, which is automatically given an equation number by \LaTeX{} like this:
 \begin{verbatim}
 \begin{equation}
diff -r a0f27e21b42c -r e5dd8cc0aa82 thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Fri Mar 25 21:49:53 2022 +0000
+++ b/thys2/ClosedForms.thy	Sat Mar 26 11:09:50 2022 +0000
@@ -494,11 +494,17 @@
 
 
 
+lemma rflts_fltsder_derflts:
+  shows "rflts (map rsimp (rdistinct (map (rder x3) (rflts rs)) rset)) = 
+         rflts (map rsimp (rdistinct (rflts (map (rder x3) rs)) rset))"
+  sorry
+
+
 lemma simp_der_flts:
   shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) rset))= 
          rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) rset))"
 
-  apply(induct rs)
+  apply(induct rs arbitrary: rset)
    apply simp
   apply(case_tac a)
        apply simp