equal
deleted
inserted
replaced
81 val parse_patt_PIDE: theory -> string -> term (*rename to parse_patt*) |
81 val parse_patt_PIDE: theory -> string -> term (*rename to parse_patt*) |
82 (*goal*)val parse_patt: theory -> string -> term (*with typ_a2real still for tests *) |
82 (*goal*)val parse_patt: theory -> string -> term (*with typ_a2real still for tests *) |
83 (*for test/* *) |
83 (*for test/* *) |
84 (*goal*)val parse_test: Proof.context -> string -> term |
84 (*goal*)val parse_test: Proof.context -> string -> term |
85 (*goal*)val parse_patt_test: theory -> string -> term |
85 (*goal*)val parse_patt_test: theory -> string -> term |
86 val str2term: string -> term (*to be replaced by parse/_patt in src*, by parse/_patt in test/**) |
|
87 |
86 |
88 val str_of_free_opt: term -> string option |
87 val str_of_free_opt: term -> string option |
89 val str_of_int: int -> string |
88 val str_of_int: int -> string |
90 val strip_imp_prems': term -> term option |
89 val strip_imp_prems': term -> term option |
91 val subst_atomic_all: LibraryC.subst -> term -> bool * term |
90 val subst_atomic_all: LibraryC.subst -> term -> bool * term |
588 |> Model_Pattern.adapt_term_to_type ctxt |
587 |> Model_Pattern.adapt_term_to_type ctxt |
589 fun parse_patt_test thy str = (thy, str) |
588 fun parse_patt_test thy str = (thy, str) |
590 |>> Proof_Context.init_global |
589 |>> Proof_Context.init_global |
591 |-> Proof_Context.read_term_pattern |
590 |-> Proof_Context.read_term_pattern |
592 |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy) |
591 |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy) |
593 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str |
|
594 |
592 |
595 |
593 |
596 fun is_atom (Const _) = true |
594 fun is_atom (Const _) = true |
597 | is_atom (Free _) = true |
595 | is_atom (Free _) = true |
598 | is_atom (Var _) = true |
596 | is_atom (Var _) = true |