Nominal/Ex/Let.thy
changeset 2454 9ffee4eb1ae1
parent 2449 6b51117b8955
child 2490 320775fa47ca
equal deleted inserted replaced
2453:2f47291b6ff9 2454:9ffee4eb1ae1
     1 theory Let
     1 theory Let
     2 imports "../NewParser" 
     2 imports "../Nominal2" 
     3 begin
     3 begin
     4 
     4 
     5 text {* example 3 or example 5 from Terms.thy *}
     5 text {* example 3 or example 5 from Terms.thy *}
     6 
     6 
     7 atom_decl name
     7 atom_decl name