equal
deleted
inserted
replaced
91 Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT); |
91 Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT); |
92 val spec = |
92 val spec = |
93 mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}) |
93 mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}) |
94 |> Syntax.check_term lthy; |
94 |> Syntax.check_term lthy; |
95 val ((_, (_, raw_def)), lthy') = |
95 val ((_, (_, raw_def)), lthy') = |
96 Specification.definition NONE [] (Attrib.empty_binding, spec) lthy; |
96 Specification.definition NONE [] [] (Attrib.empty_binding, spec) lthy; |
97 val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy'); |
97 val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy'); |
98 val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def; |
98 val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def; |
99 in |
99 in |
100 (def, lthy') |
100 (def, lthy') |
101 end; |
101 end; |