equal
deleted
inserted
replaced
17 (*Add constants to a theory*) |
17 (*Add constants to a theory*) |
18 infix addconsts; |
18 infix addconsts; |
19 fun thy addconsts const_decs = |
19 fun thy addconsts const_decs = |
20 extend_theory thy (space_implode "_" (flat (map #1 const_decs)) |
20 extend_theory thy (space_implode "_" (flat (map #1 const_decs)) |
21 ^ "_Theory") |
21 ^ "_Theory") |
22 ([], [], [], [], const_decs, None) []; |
22 ([], [], [], [], [], const_decs, None) []; |
23 |
23 |
24 |
24 |
25 (*Make a definition, lhs==rhs, checking that vars on lhs contain *) |
25 (*Make a definition, lhs==rhs, checking that vars on lhs contain *) |
26 fun mk_defpair sign (lhs,rhs) = |
26 fun mk_defpair sign (lhs,rhs) = |
27 let val Const(name,_) = head_of lhs |
27 let val Const(name,_) = head_of lhs |