doc-src/TutorialI/Ifexpr/ROOT.ML
changeset 8745 13b32661dde4
child 9834 109b11c4e77e
equal deleted inserted replaced
8744:22fa8b16c3ae 8745:13b32661dde4
       
     1 use_thy "Ifexpr";