src/HOL/HoareParallel/Graph.thy
changeset 16417 9bc16273c2d4
parent 13601 fd3e3d6b37b2
child 20217 25b068a99d2b
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     1 
     1 
     2 header {* \chapter{Case Study: Single and Multi-Mutator Garbage Collection Algorithms}
     2 header {* \chapter{Case Study: Single and Multi-Mutator Garbage Collection Algorithms}
     3 
     3 
     4 \section {Formalization of the Memory} *}
     4 \section {Formalization of the Memory} *}
     5 
     5 
     6 theory Graph = Main:
     6 theory Graph imports Main begin
     7 
     7 
     8 datatype node = Black | White
     8 datatype node = Black | White
     9 
     9 
    10 types 
    10 types 
    11   nodes = "node list"
    11   nodes = "node list"