equal
deleted
inserted
replaced
61 val mk_num_op_num: typ -> typ -> string * typ -> int -> int -> term |
61 val mk_num_op_num: typ -> typ -> string * typ -> int -> int -> term |
62 val mk_num_op_var: term -> string -> typ -> typ -> int -> term |
62 val mk_num_op_var: term -> string -> typ -> typ -> int -> term |
63 val mk_var_op_num: term -> string -> typ -> typ -> int -> term |
63 val mk_var_op_num: term -> string -> typ -> typ -> int -> term |
64 |
64 |
65 val matches: theory -> term -> term -> bool |
65 val matches: theory -> term -> term -> bool |
|
66 val parse_strict: theory -> string -> term |
66 val parse: theory -> string -> cterm option |
67 val parse: theory -> string -> cterm option |
67 val parseN: theory -> string -> cterm option |
68 val parseN: theory -> string -> cterm option |
68 val parseNEW: Proof.context -> string -> term option |
69 val parseNEW: Proof.context -> string -> term option |
69 val parseNEW': Proof.context -> string -> term |
70 val parseNEW': Proof.context -> string -> term |
70 val parseNEW'': theory -> string -> term |
71 val parseNEW'': theory -> string -> term |
502 in Thm.global_cterm_of thy t end\<close>; |
503 in Thm.global_cterm_of thy t end\<close>; |
503 fun parseN thy str = (* introduced 2002 *) |
504 fun parseN thy str = (* introduced 2002 *) |
504 \<^try>\<open> |
505 \<^try>\<open> |
505 let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str) |
506 let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str) |
506 in Thm.global_cterm_of thy t end\<close>; |
507 in Thm.global_cterm_of thy t end\<close>; |
|
508 |
|
509 fun parse_strict thy str = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str); |
507 fun parse thy str = (* introduced 2010 *) |
510 fun parse thy str = (* introduced 2010 *) |
508 \<^try>\<open> |
511 \<^try>\<open> |
509 let val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str) |
512 let val t = parse_strict thy str |
510 in Thm.global_cterm_of thy t end\<close>; |
513 in Thm.global_cterm_of thy t end\<close>; |
511 |
514 |
512 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*) |
515 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*) |
513 fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str |> numbers_to_string\<close>; |
516 fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str |> numbers_to_string\<close>; |
514 fun parseNEW' ctxt str = |
517 fun parseNEW' ctxt str = |