equal
deleted
inserted
replaced
75 |
75 |
76 val size_of = Symtab.lookup o Data.get o Context.Proof; |
76 val size_of = Symtab.lookup o Data.get o Context.Proof; |
77 val size_of_global = Symtab.lookup o Data.get o Context.Theory; |
77 val size_of_global = Symtab.lookup o Data.get o Context.Theory; |
78 |
78 |
79 fun all_overloaded_size_defs_of ctxt = |
79 fun all_overloaded_size_defs_of ctxt = |
80 Symtab.fold (fn (_, (_, (overloaded_size_def, _, _))) => cons overloaded_size_def) |
80 Symtab.fold (fn (_, (_, (overloaded_size_def, _, _))) => |
|
81 can (Logic.dest_equals o Thm.prop_of) overloaded_size_def ? cons overloaded_size_def) |
81 (Data.get (Context.Proof ctxt)) []; |
82 (Data.get (Context.Proof ctxt)) []; |
82 |
83 |
83 val size_gen_o_map_simps = @{thms inj_on_id snd_comp_apfst[unfolded apfst_def]}; |
84 val size_gen_o_map_simps = @{thms inj_on_id snd_comp_apfst[unfolded apfst_def]}; |
84 |
85 |
85 fun mk_size_gen_o_map_tac ctxt size_def rec_o_map inj_maps size_maps = |
86 fun mk_size_gen_o_map_tac ctxt size_def rec_o_map inj_maps size_maps = |