equal
deleted
inserted
replaced
67 infix 0 :== ===; |
67 infix 0 :== ===; |
68 |
68 |
69 val (op :==) = Logic.mk_defpair; |
69 val (op :==) = Logic.mk_defpair; |
70 val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
70 val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
71 |
71 |
72 fun lambda v t = |
|
73 let val (x, T) = Term.dest_Free v |
|
74 in Abs (x, T, abstract_over (v, t)) end; |
|
75 |
|
76 fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname); |
72 fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname); |
77 |
73 |
78 |
74 |
79 (* proof by simplification *) |
75 (* proof by simplification *) |
80 |
76 |