equal
deleted
inserted
replaced
91 val def = singleton (Proof_Context.export lthy' ctxt_thy) raw_def; |
91 val def = singleton (Proof_Context.export lthy' ctxt_thy) raw_def; |
92 in |
92 in |
93 (def, lthy') |
93 (def, lthy') |
94 end; |
94 end; |
95 |
95 |
96 fun tac ctxt thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms); |
96 fun tac ctxt thms = |
|
97 Class.intro_classes_tac ctxt [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms); |
97 |
98 |
98 val qualify = |
99 val qualify = |
99 Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name; |
100 Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name; |
100 in |
101 in |
101 Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal]) |
102 Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal]) |