equal
deleted
inserted
replaced
1 theory Nominal |
1 theory Nominal |
2 imports Main Infinite_Set |
2 imports Main Infinite_Set |
3 uses |
3 uses |
4 ("nominal_thmdecls.ML") |
4 ("nominal_thmdecls.ML") |
5 ("nominal_atoms.ML") |
5 ("nominal_atoms.ML") |
6 ("nominal_package.ML") |
6 ("nominal.ML") |
7 ("nominal_induct.ML") |
7 ("nominal_induct.ML") |
8 ("nominal_permeq.ML") |
8 ("nominal_permeq.ML") |
9 ("nominal_fresh_fun.ML") |
9 ("nominal_fresh_fun.ML") |
10 ("nominal_primrec.ML") |
10 ("nominal_primrec.ML") |
11 ("nominal_inductive.ML") |
11 ("nominal_inductive.ML") |
3668 (************************************************) |
3668 (************************************************) |
3669 (* main file for constructing nominal datatypes *) |
3669 (* main file for constructing nominal datatypes *) |
3670 lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []" |
3670 lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []" |
3671 using assms .. |
3671 using assms .. |
3672 |
3672 |
3673 use "nominal_package.ML" |
3673 use "nominal.ML" |
3674 |
3674 |
3675 (******************************************************) |
3675 (******************************************************) |
3676 (* primitive recursive functions on nominal datatypes *) |
3676 (* primitive recursive functions on nominal datatypes *) |
3677 use "nominal_primrec.ML" |
3677 use "nominal_primrec.ML" |
3678 |
3678 |