equal
deleted
inserted
replaced
2 imports |
2 imports |
3 Nominal2_Base Nominal2_Eqvt Nominal2_Abs |
3 Nominal2_Base Nominal2_Eqvt Nominal2_Abs |
4 uses ("nominal_dt_rawfuns.ML") |
4 uses ("nominal_dt_rawfuns.ML") |
5 ("nominal_dt_alpha.ML") |
5 ("nominal_dt_alpha.ML") |
6 ("nominal_dt_quot.ML") |
6 ("nominal_dt_quot.ML") |
|
7 ("induction_schema.ML") |
7 begin |
8 begin |
8 |
9 |
|
10 use "induction_schema.ML" |
9 |
11 |
10 use "nominal_dt_rawfuns.ML" |
12 use "nominal_dt_rawfuns.ML" |
11 ML {* open Nominal_Dt_RawFuns *} |
13 ML {* open Nominal_Dt_RawFuns *} |
12 |
14 |
13 use "nominal_dt_alpha.ML" |
15 use "nominal_dt_alpha.ML" |
531 |
533 |
532 (* proving the strong exhausts and induct lemmas *) |
534 (* proving the strong exhausts and induct lemmas *) |
533 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' |
535 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' |
534 qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms |
536 qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms |
535 |
537 |
536 val qstrong_induct_thm = prove_strong_induct lthyC qinduct qexhausts bclauses |
538 val qstrong_induct_thm = prove_strong_induct lthyC qinduct qstrong_exhaust_thms bclauses |
537 |
539 |
538 |
540 |
539 (* noting the theorems *) |
541 (* noting the theorems *) |
540 |
542 |
541 (* generating the prefix for the theorem names *) |
543 (* generating the prefix for the theorem names *) |