equal
deleted
inserted
replaced
149 ||> TheoryTarget.instantiation |
149 ||> TheoryTarget.instantiation |
150 (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size]) |
150 (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size]) |
151 ||>> fold_map define_overloaded |
151 ||>> fold_map define_overloaded |
152 (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1)) |
152 (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1)) |
153 ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
153 ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
154 ||> LocalTheory.exit |
154 ||> LocalTheory.exit_global; |
155 ||> ProofContext.theory_of; |
|
156 |
155 |
157 val ctxt = ProofContext.init thy'; |
156 val ctxt = ProofContext.init thy'; |
158 |
157 |
159 val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm add_0_right} :: |
158 val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm add_0_right} :: |
160 size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites; |
159 size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites; |