equal
deleted
inserted
replaced
14 | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts; |
14 | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts; |
15 |
15 |
16 (*Make a definition lhs==rhs*) |
16 (*Make a definition lhs==rhs*) |
17 fun mk_defpair (lhs, rhs) = |
17 fun mk_defpair (lhs, rhs) = |
18 let val Const(name, _) = head_of lhs |
18 let val Const(name, _) = head_of lhs |
19 in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end; |
19 in (Sign.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) end; |
20 |
20 |
21 fun get_def thy s = get_axiom thy (s^"_def"); |
21 fun get_def thy s = get_axiom thy (s^"_def"); |
22 |
22 |
23 |
23 |
24 (*Read an assumption in the given theory*) |
24 (*Read an assumption in the given theory*) |