src/HOL/MicroJava/J/JListExample.thy
changeset 46512 4f9f61f9b535
parent 46506 c7faa011bfa7
child 51272 9c8d63b4b6be
equal deleted inserted replaced
46511:fbb3c68a8d3c 46512:4f9f61f9b535
     6 
     6 
     7 theory JListExample
     7 theory JListExample
     8 imports Eval
     8 imports Eval
     9 begin
     9 begin
    10 
    10 
    11 declare [[syntax_ambiguity = ignore]]
    11 declare [[syntax_ambiguity_warning = false]]
    12 
    12 
    13 consts
    13 consts
    14   list_nam :: cnam
    14   list_nam :: cnam
    15   append_name :: mname
    15   append_name :: mname
    16 
    16