equal
deleted
inserted
replaced
7 "../SizeBound4" |
7 "../SizeBound4" |
8 "HOL-Library.LaTeXsugar" |
8 "HOL-Library.LaTeXsugar" |
9 begin |
9 begin |
10 |
10 |
11 declare [[show_question_marks = false]] |
11 declare [[show_question_marks = false]] |
|
12 |
|
13 notation (latex output) |
|
14 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 |
|
15 Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) |
|
16 |
12 |
17 |
13 abbreviation |
18 abbreviation |
14 "der_syn r c \<equiv> der c r" |
19 "der_syn r c \<equiv> der c r" |
15 |
20 |
16 notation (latex output) |
21 notation (latex output) |
155 text {* |
160 text {* |
156 not direct correspondence with PDERs, because of example |
161 not direct correspondence with PDERs, because of example |
157 problem with retrieve |
162 problem with retrieve |
158 |
163 |
159 correctness |
164 correctness |
|
165 |
|
166 |
|
167 |
|
168 \begin{figure}[t] |
|
169 \begin{center} |
|
170 \begin{tabular}{c} |
|
171 @{thm[mode=Axiom] bs1}\qquad |
|
172 @{thm[mode=Axiom] bs2}\qquad |
|
173 @{thm[mode=Axiom] bs3}\\ |
|
174 @{thm[mode=Rule] bs4}\qquad |
|
175 @{thm[mode=Rule] bs5}\\ |
|
176 @{thm[mode=Rule] bs6}\qquad |
|
177 @{thm[mode=Rule] bs7}\\ |
|
178 @{thm[mode=Rule] bs8}\\ |
|
179 @{thm[mode=Axiom] ss1}\qquad |
|
180 @{thm[mode=Rule] ss2}\qquad |
|
181 @{thm[mode=Rule] ss3}\\ |
|
182 @{thm[mode=Axiom] ss4}\qquad |
|
183 @{thm[mode=Axiom] ss5}\qquad |
|
184 @{thm[mode=Rule] ss6}\\ |
|
185 \end{tabular} |
|
186 \end{center} |
|
187 \caption{???}\label{SimpRewrites} |
|
188 \end{figure} |
160 *} |
189 *} |
161 |
190 |
162 section {* Bound - NO *} |
191 section {* Bound - NO *} |
163 |
192 |
164 section {* Bounded Regex / Not *} |
193 section {* Bounded Regex / Not *} |