equal
deleted
inserted
replaced
1 theory NewParser |
1 theory NewParser |
2 imports "../Nominal-General/Nominal2_Base" |
2 imports "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal-General/Nominal2_Supp" |
4 "../Nominal-General/Nominal2_Supp" |
5 "Perm" "NewAlpha" "Tacs" "Equivp" "Lift" |
5 "Perm" "Tacs" "Equivp" "Lift" |
6 begin |
6 begin |
7 |
7 |
8 |
8 |
9 section{* Interface for nominal_datatype *} |
9 section{* Interface for nominal_datatype *} |
10 |
10 |
349 else raise TEST lthy3 |
349 else raise TEST lthy3 |
350 |
350 |
351 (* definition of raw alphas *) |
351 (* definition of raw alphas *) |
352 val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
352 val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
353 if get_STEPS lthy > 4 |
353 if get_STEPS lthy > 4 |
354 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs raw_fv_bns lthy3a |
354 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a |
355 else raise TEST lthy3a |
355 else raise TEST lthy3a |
356 |
356 |
357 val (alpha_ts_nobn, alpha_ts_bn) = chop (length raw_fvs) alpha_ts |
357 val (alpha_ts_nobn, alpha_ts_bn) = chop (length raw_fvs) alpha_ts |
358 |
358 |
359 val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; |
359 val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; |