equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 section {* Parsing and Typing the Specification\label{sec:interface} *} |
5 section {* Parsing and Typing the Specification\label{sec:interface} *} |
6 |
6 |
7 text_raw {* |
7 text_raw {* |
8 \begin{figure}[p] |
8 \begin{figure}[t] |
9 \begin{boxedminipage}{\textwidth} |
9 \begin{boxedminipage}{\textwidth} |
10 \begin{isabelle} |
10 \begin{isabelle} |
11 *} |
11 *} |
12 simple_inductive |
12 simple_inductive |
13 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
13 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |