equal
deleted
inserted
replaced
6 |
6 |
7 header {* \isaheader{Correctness of the LBV} *} |
7 header {* \isaheader{Correctness of the LBV} *} |
8 |
8 |
9 theory LBVCorrect = LBVSpec + Typing_Framework: |
9 theory LBVCorrect = LBVSpec + Typing_Framework: |
10 |
10 |
11 locale lbvs = lbv + |
11 locale (open) lbvs = lbv + |
12 fixes s0 :: 'a |
12 fixes s0 :: 'a |
13 fixes c :: "'a list" |
13 fixes c :: "'a list" |
14 fixes ins :: "'b list" |
14 fixes ins :: "'b list" |
15 fixes phi :: "'a list" ("\<phi>") |
15 fixes phi :: "'a list" ("\<phi>") |
16 defines phi_def: |
16 defines phi_def: |