equal
deleted
inserted
replaced
55 introduction rules short as @{text "rules"}. Borrowing some idealised Isabelle |
55 introduction rules short as @{text "rules"}. Borrowing some idealised Isabelle |
56 notation, one such @{text "rule"} is assumed to be of the form |
56 notation, one such @{text "rule"} is assumed to be of the form |
57 |
57 |
58 \begin{isabelle} |
58 \begin{isabelle} |
59 @{text "rule ::= |
59 @{text "rule ::= |
60 \<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow> |
60 \<And>xs. \<^latex>\<open>$\\underbrace{\\mbox{\<close>As\<^latex>\<open>}}_{\\text{\\makebox[0mm]{\\rm non-recursive premises}}}$\<close> \<Longrightarrow> |
61 \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^raw:}}_{\text{\rm recursive premises}}$> |
61 \<^latex>\<open>$\\underbrace{\\mbox{\<close>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^latex>\<open>}}_{\\text{\\rm recursive premises}}$>\<close> |
62 \<Longrightarrow> pred ts"} |
62 \<Longrightarrow> pred ts"} |
63 \end{isabelle} |
63 \end{isabelle} |
64 |
64 |
65 For the purposes here, we will assume the @{text rules} have this format and |
65 For the purposes here, we will assume the @{text rules} have this format and |
66 omit any code that actually tests this. Therefore ``things'' can go horribly |
66 omit any code that actually tests this. Therefore ``things'' can go horribly |