src/HOL/Imperative_HOL/ex/Linked_Lists.thy
changeset 35041 6eb917794a5c
parent 34051 1a82e2e29d67
child 35423 6ef9525a5727
equal deleted inserted replaced
35039:e682bb587071 35041:6eb917794a5c
   984     ll_zs \<leftarrow> !p;
   984     ll_zs \<leftarrow> !p;
   985     zs \<leftarrow> traverse ll_zs;
   985     zs \<leftarrow> traverse ll_zs;
   986     return zs
   986     return zs
   987   done)"
   987   done)"
   988 
   988 
       
   989 code_reserved SML upto
       
   990 
   989 ML {* @{code test_1} () *}
   991 ML {* @{code test_1} () *}
   990 ML {* @{code test_2} () *}
   992 ML {* @{code test_2} () *}
   991 ML {* @{code test_3} () *}
   993 ML {* @{code test_3} () *}
   992 
   994 
   993 end
   995 end