src/HOL/Boogie/ROOT.ML
changeset 33419 8ae45e87b992
child 33615 261abc2e3155
equal deleted inserted replaced
33418:1312e8337ce5 33419:8ae45e87b992
       
     1 use_thy "Boogie";