equal
deleted
inserted
replaced
502 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
502 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
503 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars] |
503 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars] |
504 thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps |
504 thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps |
505 |
505 |
506 |
506 |
507 |
507 (* some further tests *) |
508 |
508 |
509 end |
509 nominal_datatype lam = |
510 |
510 Var "name" |
511 |
511 | App "lam" "lam list" |
512 |
512 | Lam x::"name" t::"lam" bind x in t |
|
513 |
|
514 nominal_datatype ty = |
|
515 Var "name" |
|
516 | Fun "ty" "ty" |
|
517 |
|
518 nominal_datatype tys = |
|
519 All xs::"name fset" ty::"ty_raw" bind xs in ty |
|
520 |
|
521 |
|
522 |
|
523 end |
|
524 |
|
525 |
|
526 |