src/HOL/Boogie/Examples/ROOT.ML
author haftmann
Thu, 22 Jul 2010 17:26:22 +0200
changeset 37934 440114da2488
parent 34068 a78307d72e58
permissions -rw-r--r--
dedicated exec ... syntax for open state monad (partly already introduces in d00a3f47b607)

use_thys ["Boogie_Max_Stepwise", "Boogie_Max", "Boogie_Dijkstra", "VCC_Max"];