Nominal/Ex/Lambda.thy
changeset 2311 4da5c5c29009
parent 2173 477293d841e8
child 2424 621ebd8b13c4
equal deleted inserted replaced
2310:dd3b9c046c7d 2311:4da5c5c29009
     1 theory Lambda
     1 theory Lambda
     2 imports "../NewParser" Quotient_Option
     2 imports "../NewParser" Quotient_Option
     3 begin
     3 begin
     4 
     4 
     5 atom_decl name
     5 atom_decl name
       
     6 declare [[STEPS = 9]]
     6 
     7 
     7 nominal_datatype lam =
     8 nominal_datatype lam =
     8   Var "name"
     9   Var "name"
     9 | App "lam" "lam"
    10 | App "lam" "lam"
    10 | Lam x::"name" l::"lam"  bind_set x in l
    11 | Lam x::"name" l::"lam"  bind x in l
    11 
    12 
    12 thm lam.fv
    13 thm lam.fv
    13 thm lam.supp
    14 thm lam.supp
    14 lemmas supp_fn' = lam.fv[simplified lam.supp]
    15 lemmas supp_fn' = lam.fv[simplified lam.supp]
    15 
    16