equal
deleted
inserted
replaced
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{Correctness of the LBV} *} |
7 header {* \isaheader{Correctness of the LBV} *} |
8 |
8 |
9 theory LBVCorrect imports LBVSpec Typing_Framework begin |
9 theory LBVCorrect |
10 |
10 imports LBVSpec Typing_Framework |
11 locale (open) lbvs = lbv + |
11 begin |
|
12 |
|
13 locale lbvs = lbv + |
12 fixes s0 :: 'a ("s\<^sub>0") |
14 fixes s0 :: 'a ("s\<^sub>0") |
13 fixes c :: "'a list" |
15 fixes c :: "'a list" |
14 fixes ins :: "'b list" |
16 fixes ins :: "'b list" |
15 fixes phi :: "'a list" ("\<phi>") |
17 fixes phi :: "'a list" ("\<phi>") |
16 defines phi_def: |
18 defines phi_def: |