src/HOL/Library/ExecutableSet.thy
changeset 21875 5df10a17644e
parent 21572 7442833ea2b6
child 21911 e29bcab0c81c
equal deleted inserted replaced
21874:aa350df2372c 21875:5df10a17644e
   269 section {* code generator setup *}
   269 section {* code generator setup *}
   270 
   270 
   271 ML {*
   271 ML {*
   272 nonfix inter;
   272 nonfix inter;
   273 nonfix union;
   273 nonfix union;
       
   274 nonfix subset;
   274 *}
   275 *}
   275 
   276 
   276 code_modulename SML
   277 code_modulename SML
   277   ExecutableSet List
   278   ExecutableSet List
   278   Set List
   279   Set List