equal
deleted
inserted
replaced
68 asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW |
68 asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW |
69 TRY o blast_tac (claset_of ctxt) |
69 TRY o blast_tac (claset_of ctxt) |
70 *} |
70 *} |
71 |
71 |
72 ML {* |
72 ML {* |
73 fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt) |
73 fun sym_eqvts ctxt = maps (fn x => [sym OF [x]] handle _ => []) (Nominal_ThmDecls.get_eqvts_thms ctxt) |
74 fun all_eqvts ctxt = |
74 fun all_eqvts ctxt = |
75 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
75 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
76 *} |
76 *} |
77 |
77 |
78 ML {* |
78 ML {* |