440 $ Free ("x", ty) $ Free ("y", ty); |
440 $ Free ("x", ty) $ Free ("y", ty); |
441 val def = HOLogic.mk_Trueprop (HOLogic.mk_eq |
441 val def = HOLogic.mk_Trueprop (HOLogic.mk_eq |
442 (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="})); |
442 (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="})); |
443 val def' = Syntax.check_term lthy def; |
443 val def' = Syntax.check_term lthy def; |
444 val ((_, (_, thm)), lthy') = Specification.definition |
444 val ((_, (_, thm)), lthy') = Specification.definition |
445 (NONE, ((Name.no_binding, []), def')) lthy; |
445 (NONE, (Attrib.no_binding, def')) lthy; |
446 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy); |
446 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy); |
447 val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm; |
447 val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm; |
448 in (thm', lthy') end; |
448 in (thm', lthy') end; |
449 fun tac thms = Class.intro_classes_tac [] |
449 fun tac thms = Class.intro_classes_tac [] |
450 THEN ALLGOALS (ProofContext.fact_tac thms); |
450 THEN ALLGOALS (ProofContext.fact_tac thms); |