Nominal/Ex/SingleLet.thy
changeset 2479 a9b6a00b1ba0
parent 2477 2f289c1f6cf1
child 2486 b4ea19604b0b
equal deleted inserted replaced
2478:9b673588244a 2479:a9b6a00b1ba0
     1 theory SingleLet
     1 theory SingleLet
     2 imports "../Nominal2" 
     2 imports "../Nominal2" 
     3 begin
     3 begin
     4 
       
     5 ML {*
       
     6 Inductive.unpartition_rules
       
     7 *}
       
     8 
       
     9 
     4 
    10 atom_decl name
     5 atom_decl name
    11 
     6 
    12 declare [[STEPS = 100]]
     7 declare [[STEPS = 100]]
    13 
     8