equal
deleted
inserted
replaced
2 |
2 |
3 theory Spec |
3 theory Spec |
4 imports Main |
4 imports Main |
5 begin |
5 begin |
6 |
6 |
7 chapter {* Specifications *} |
7 chapter {* Theory specifications *} |
8 |
8 |
9 section {* Defining theories \label{sec:begin-thy} *} |
9 section {* Defining theories \label{sec:begin-thy} *} |
10 |
10 |
11 text {* |
11 text {* |
12 \begin{matharray}{rcl} |
12 \begin{matharray}{rcl} |
1100 |
1100 |
1101 text {* |
1101 text {* |
1102 \begin{matharray}{rcll} |
1102 \begin{matharray}{rcll} |
1103 @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ |
1103 @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ |
1104 @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\ |
1104 @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\ |
1105 @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\ |
1105 @{command_def "theorems"} & : & \isarkeep{local{\dsh}theory} \\ |
1106 \end{matharray} |
1106 \end{matharray} |
1107 |
1107 |
1108 \begin{rail} |
1108 \begin{rail} |
1109 'axioms' (axmdecl prop +) |
1109 'axioms' (axmdecl prop +) |
1110 ; |
1110 ; |
1317 general concept of syntax transformations in Isabelle. |
1317 general concept of syntax transformations in Isabelle. |
1318 |
1318 |
1319 %FIXME proper antiquotations |
1319 %FIXME proper antiquotations |
1320 \begin{ttbox} |
1320 \begin{ttbox} |
1321 val parse_ast_translation: |
1321 val parse_ast_translation: |
1322 (string * (Context.generic -> ast list -> ast)) list |
1322 (string * (Proof.context -> ast list -> ast)) list |
1323 val parse_translation: |
1323 val parse_translation: |
1324 (string * (Context.generic -> term list -> term)) list |
1324 (string * (Proof.context -> term list -> term)) list |
1325 val print_translation: |
1325 val print_translation: |
1326 (string * (Context.generic -> term list -> term)) list |
1326 (string * (Proof.context -> term list -> term)) list |
1327 val typed_print_translation: |
1327 val typed_print_translation: |
1328 (string * (Context.generic -> bool -> typ -> term list -> term)) list |
1328 (string * (Proof.context -> bool -> typ -> term list -> term)) list |
1329 val print_ast_translation: |
1329 val print_ast_translation: |
1330 (string * (Context.generic -> ast list -> ast)) list |
1330 (string * (Proof.context -> ast list -> ast)) list |
1331 \end{ttbox} |
1331 \end{ttbox} |
1332 *} |
1332 *} |
1333 |
1333 |
1334 end |
1334 end |