src/HOL/Boogie/Examples/ROOT.ML
changeset 48722 a5e3ba7cbb2a
parent 48721 866f6d5baf4c
child 48723 0829e958f0aa
equal deleted inserted replaced
48721:866f6d5baf4c 48722:a5e3ba7cbb2a
     1 use_thys ["Boogie_Max_Stepwise", "Boogie_Max", "Boogie_Dijkstra", "VCC_Max"];