equal
deleted
inserted
replaced
525 then have "v = Void" |
525 then have "v = Void" |
526 by (simp add: LV_simps) |
526 by (simp add: LV_simps) |
527 then show "Void :\<sqsubseteq>val v" |
527 then show "Void :\<sqsubseteq>val v" |
528 by (simp add: PosOrd_ex_eq_def) |
528 by (simp add: PosOrd_ex_eq_def) |
529 next |
529 next |
530 case (Posix_CHAR c v) |
530 case (Posix_CH c v) |
531 have "v \<in> LV (CHAR c) [c]" by fact |
531 have "v \<in> LV (CH c) [c]" by fact |
532 then have "v = Char c" |
532 then have "v = Char c" |
533 by (simp add: LV_simps) |
533 by (simp add: LV_simps) |
534 then show "Char c :\<sqsubseteq>val v" |
534 then show "Char c :\<sqsubseteq>val v" |
535 by (simp add: PosOrd_ex_eq_def) |
535 by (simp add: PosOrd_ex_eq_def) |
536 next |
536 next |