equal
deleted
inserted
replaced
22 thm lam_bp_fv |
22 thm lam_bp_fv |
23 thm lam_bp_inject |
23 thm lam_bp_inject |
24 thm lam_bp_bn |
24 thm lam_bp_bn |
25 thm lam_bp_perm |
25 thm lam_bp_perm |
26 thm lam_bp_induct |
26 thm lam_bp_induct |
|
27 thm lam_bp_inducts |
27 thm lam_bp_distinct |
28 thm lam_bp_distinct |
28 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
29 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
29 |
30 |
30 term "supp (x :: lam)" |
31 term "supp (x :: lam)" |
31 lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted] |
|
32 |
32 |
33 (* maybe should be added to Infinite.thy *) |
33 (* maybe should be added to Infinite.thy *) |
34 lemma infinite_Un: |
34 lemma infinite_Un: |
35 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
35 shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
36 by simp |
36 by simp |
304 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv |
304 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv |
305 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject |
305 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject |
306 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn |
306 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn |
307 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm |
307 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm |
308 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct |
308 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct |
|
309 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inducts |
309 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct |
310 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct |
310 |
311 |
311 (* example 3 from Peter Sewell's bestiary *) |
312 (* example 3 from Peter Sewell's bestiary *) |
312 |
313 |
313 nominal_datatype exp = |
314 nominal_datatype exp = |