diff -r e1b74d618f1b -r dac6d27c99c6 thys2/Paper/Paper.thy
--- a/thys2/Paper/Paper.thy	Thu Jan 27 23:25:26 2022 +0000
+++ b/thys2/Paper/Paper.thy	Fri Jan 28 12:02:25 2022 +0000
@@ -10,6 +10,11 @@
 
 declare [[show_question_marks = false]]
 
+notation (latex output)
+  If  ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and
+  Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) 
+
+
 abbreviation 
   "der_syn r c \<equiv> der c r"
 
@@ -157,6 +162,30 @@
    problem with retrieve 
 
    correctness
+
+
+
+   \begin{figure}[t]
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=Axiom] bs1}\qquad
+  @{thm[mode=Axiom] bs2}\qquad
+  @{thm[mode=Axiom] bs3}\\
+  @{thm[mode=Rule] bs4}\qquad
+  @{thm[mode=Rule] bs5}\\
+  @{thm[mode=Rule] bs6}\qquad
+  @{thm[mode=Rule] bs7}\\
+  @{thm[mode=Rule] bs8}\\
+  @{thm[mode=Axiom] ss1}\qquad
+  @{thm[mode=Rule] ss2}\qquad
+  @{thm[mode=Rule] ss3}\\
+  @{thm[mode=Axiom] ss4}\qquad
+  @{thm[mode=Axiom] ss5}\qquad
+  @{thm[mode=Rule] ss6}\\
+  \end{tabular}
+  \end{center}
+  \caption{???}\label{SimpRewrites}
+  \end{figure}
 *}
 
 section {* Bound - NO *}