equal
deleted
inserted
replaced
3 Copyright 1996 TUM |
3 Copyright 1996 TUM |
4 *) |
4 *) |
5 |
5 |
6 section "Denotational Semantics of Commands in HOLCF" |
6 section "Denotational Semantics of Commands in HOLCF" |
7 |
7 |
8 theory Denotational imports HOLCF "~~/src/HOL/IMP/Big_Step" begin |
8 theory Denotational imports HOLCF "HOL-IMP.Big_Step" begin |
9 |
9 |
10 subsection "Definition" |
10 subsection "Definition" |
11 |
11 |
12 definition |
12 definition |
13 dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where |
13 dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where |