Nominal/Ex/Lambda.thy
changeset 2425 715ab84065a0
parent 2424 621ebd8b13c4
child 2431 331873ebc5cd
equal deleted inserted replaced
2424:621ebd8b13c4 2425:715ab84065a0
     1 theory Lambda
     1 theory Lambda
     2 imports "../NewParser" 
     2 imports "../NewParser" 
     3 begin
     3 begin
     4 
     4 
     5 atom_decl name
     5 atom_decl name
     6 declare [[STEPS = 20]]
     6 declare [[STEPS = 2]]
     7 
     7 
     8 nominal_datatype  lam =
     8 nominal_datatype 'a lam =
     9   Var "name"
     9   Var "name"
    10 | App "lam" "lam"
    10 | App "'a lam" "'a lam"
    11 | Lam x::"name" l::"lam"  bind x in l
    11 | Lam x::"name" l::"'a lam"  bind x in l
       
    12 
       
    13 ML {* Datatype.read_typ *}
    12 
    14 
    13 
    15 
    14 thm eq_iff
    16 thm eq_iff
    15 
    17 
    16 thm lam.fv
    18 thm lam.fv