src/HOL/Library/Transitive_Closure_Table.thy
changeset 44844 a907e541b127
parent 37589 9c33d02656bc
child 45761 22f665a2e91c
equal deleted inserted replaced
44841:3d204d261903 44844:a907e541b127
   199 where
   199 where
   200   "test A B"
   200   "test A B"
   201 | "test B A"
   201 | "test B A"
   202 | "test B C"
   202 | "test B C"
   203 
   203 
   204 subsubsection {* Invoking with the SML code generator *}
   204 subsubsection {* Invoking with the (legacy) SML code generator *}
       
   205 
       
   206 text {* this test can be removed once the SML code generator is deactivated *}
   205 
   207 
   206 code_module Test
   208 code_module Test
   207 contains
   209 contains
   208 test1 = "test\<^sup>*\<^sup>* A C"
   210 test1 = "test\<^sup>*\<^sup>* A C"
   209 test2 = "test\<^sup>*\<^sup>* C A"
   211 test2 = "test\<^sup>*\<^sup>* C A"