equal
deleted
inserted
replaced
20 val term_vars: term -> term list |
20 val term_vars: term -> term list |
21 val add_term_frees: term * term list -> term list |
21 val add_term_frees: term * term list -> term list |
22 val term_frees: term -> term list |
22 val term_frees: term -> term list |
23 val mk_defpair: term * term -> string * term |
23 val mk_defpair: term * term -> string * term |
24 val get_def: theory -> xstring -> thm |
24 val get_def: theory -> xstring -> thm |
25 val simple_read_term: theory -> typ -> string -> term |
|
26 val METAHYPS: (thm list -> tactic) -> int -> tactic |
25 val METAHYPS: (thm list -> tactic) -> int -> tactic |
27 end; |
26 end; |
28 |
27 |
29 structure Misc_Legacy: MISC_LEGACY = |
28 structure Misc_Legacy: MISC_LEGACY = |
30 struct |
29 struct |
100 (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) |
99 (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) |
101 | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); |
100 | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); |
102 |
101 |
103 |
102 |
104 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name; |
103 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name; |
105 |
|
106 |
|
107 fun simple_read_term thy T s = |
|
108 let |
|
109 val ctxt = Proof_Context.init_global thy |
|
110 |> Proof_Context.allow_dummies |
|
111 |> Proof_Context.set_mode Proof_Context.mode_schematic; |
|
112 val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term; |
|
113 in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end; |
|
114 |
104 |
115 |
105 |
116 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions |
106 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions |
117 METAHYPS (fn prems => tac prems) i |
107 METAHYPS (fn prems => tac prems) i |
118 |
108 |