70 val mk_num_op_var: term -> string -> typ -> typ -> int -> term |
70 val mk_num_op_var: term -> string -> typ -> typ -> int -> term |
71 val mk_var_op_num: term -> string -> typ -> typ -> int -> term |
71 val mk_var_op_num: term -> string -> typ -> typ -> int -> term |
72 |
72 |
73 val matches: theory -> term -> term -> bool |
73 val matches: theory -> term -> term -> bool |
74 |
74 |
75 val parse: Proof.context -> string -> term |
75 (*val parse_patt: theory -> string -> term \<longrightarrow> ParseC.patt_opt *) |
76 val parse_patt: theory -> string -> term |
|
77 (*val parse_opt: Proof.context -> string -> term option (*kept while developing Specify*)*) |
76 (*val parse_opt: Proof.context -> string -> term option (*kept while developing Specify*)*) |
78 val parseNEW: Proof.context -> string -> term option |
77 val parseNEW: Proof.context -> string -> term option |
79 val parseNEW': Proof.context -> string -> term (*old version to be eliminated*) |
78 val parseNEW': Proof.context -> string -> term (*old version to be eliminated*) |
80 val parseNEW'': theory -> string -> term (*old version to be eliminated*) |
79 val parseNEW'': theory -> string -> term (*old version to be eliminated*) |
81 (*for test/* *) |
|
82 |
80 |
83 val str_of_free_opt: term -> string option |
81 val str_of_free_opt: term -> string option |
84 val str_of_int: int -> string |
82 val str_of_int: int -> string |
85 val strip_imp_prems': term -> term option |
83 val strip_imp_prems': term -> term option |
86 val subst_atomic_all: LibraryC.subst -> term -> bool * term |
84 val subst_atomic_all: LibraryC.subst -> term -> bool * term |
526 case parseNEW (Proof_Context.init_global thy) str of |
524 case parseNEW (Proof_Context.init_global thy) str of |
527 SOME t => t |
525 SOME t => t |
528 | NONE => raise TERM ("NO parseNEW'' for " ^ str, []) |
526 | NONE => raise TERM ("NO parseNEW'' for " ^ str, []) |
529 (*\----- old versions to be eliminated -------------------------------------------------------/*) |
527 (*\----- old versions to be eliminated -------------------------------------------------------/*) |
530 |
528 |
531 (* to be replaced by Syntax.read_term..*) |
|
532 fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str; |
|
533 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *) |
529 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *) |
534 fun parse_patt thy str = (thy, str) |
530 fun parse_patt thy str = (thy, str) |
535 |>> Proof_Context.init_global |
531 |>> Proof_Context.init_global |
536 |-> Proof_Context.read_term_pattern |
532 |-> Proof_Context.read_term_pattern |
537 |
533 |