HomeIsabelle/Phabricator
Diffusion afp-devel e2c29c8b2469

RealTimeDeque: Separate implementation and auxiliary functions
e2c29c8b2469
Actions

Description

RealTimeDeque: Separate implementation and auxiliary functions

Details

Provenance
Balazs Toth <balazs.toth@quickbirdstudios.com>Authored on
Parents
rAFPfa7371329b67: Backed out changeset 3a67df508397
Branches
Unknown
Tags
Unknown

Changes (30)

PathSize

rAFPe2c29c8b2469

View Options

thys/Real_Time_Deque/Big.thy

Loading...
View Options

thys/Real_Time_Deque/Big_Aux.thy

Loading...
View Options

thys/Real_Time_Deque/Big_Proof.thy

Loading...
View Options

thys/Real_Time_Deque/Common.thy

Loading...
View Options

thys/Real_Time_Deque/Common_Aux.thy

Loading...
View Options

thys/Real_Time_Deque/Common_Proof.thy

Loading...
View Options

thys/Real_Time_Deque/Current.thy

Loading...
View Options

thys/Real_Time_Deque/Current_Aux.thy

Loading...
View Options

thys/Real_Time_Deque/Current_Proof.thy

Loading...
View Options

thys/Real_Time_Deque/Idle.thy

Loading...
View Options

thys/Real_Time_Deque/Idle_Aux.thy

Loading...
View Options

thys/Real_Time_Deque/Idle_Proof.thy

Loading...
View Options

thys/Real_Time_Deque/RealTimeDeque.thy

Loading...
View Options

thys/Real_Time_Deque/RealTimeDeque_Aux.thy

Loading...
View Options

thys/Real_Time_Deque/RealTimeDeque_Dequeue.thy

Loading...
View Options

thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy

Loading...
View Options

thys/Real_Time_Deque/RealTimeDeque_Enqueue.thy

Loading...
View Options

thys/Real_Time_Deque/RealTimeDeque_Enqueue_Proof.thy

Loading...
View Options

thys/Real_Time_Deque/RealTimeDeque_Proof.thy

Loading...
View Options

thys/Real_Time_Deque/Small.thy

Loading...
View Options

thys/Real_Time_Deque/Small_Aux.thy

Loading...
View Options

thys/Real_Time_Deque/Small_Proof.thy

Loading...
View Options

thys/Real_Time_Deque/Stack.thy

Loading...
View Options

thys/Real_Time_Deque/Stack_Aux.thy

Loading...
View Options

thys/Real_Time_Deque/Stack_Proof.thy

Loading...
View Options

thys/Real_Time_Deque/States.thy

Loading...
View Options

thys/Real_Time_Deque/States_Aux.thy

Loading...
View Options

thys/Real_Time_Deque/States_Proof.thy

Loading...