97 val atomtyp(*<-- atom_typ TODO*): typ -> unit |
97 val atomtyp(*<-- atom_typ TODO*): typ -> unit |
98 val atomty: term -> unit |
98 val atomty: term -> unit |
99 val atomw: term -> unit |
99 val atomw: term -> unit |
100 val atomt: term -> unit |
100 val atomt: term -> unit |
101 val atomwy: term -> unit |
101 val atomwy: term -> unit |
102 val atomty_thy: ThyC.thyID -> term -> unit |
102 val atomty_thy: ThyC.id -> term -> unit |
103 val free2var: term -> term |
103 val free2var: term -> term |
104 val contains_one_of: thm * (string * typ) list -> bool |
104 val contains_one_of: thm * (string * typ) list -> bool |
105 val contains_Const_typeless: term list -> term -> bool |
105 val contains_Const_typeless: term list -> term -> bool |
106 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
106 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
107 val typ_a2real: term -> term |
107 val typ_a2real: term -> term |
506 |
506 |
507 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation |
507 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation |
508 WN130613 probably compare to |
508 WN130613 probably compare to |
509 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*) |
509 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*) |
510 fun parse_patt thy str = (thy, str) |
510 fun parse_patt thy str = (thy, str) |
511 |>> ThyC.thy2ctxt |
511 |>> ThyC.to_ctxt |
512 |-> Proof_Context.read_term_pattern |
512 |-> Proof_Context.read_term_pattern |
513 |> numbers_to_string (*TODO drop*) |
513 |> numbers_to_string (*TODO drop*) |
514 |> typ_a2real; (*TODO drop*) |
514 |> typ_a2real; (*TODO drop*) |
515 fun str2term str = parse_patt (ThyC.Thy_Info_get_theory "Isac_Knowledge") str |
515 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str |
516 |
516 |
517 (* TODO decide with Test_Isac *) |
517 (* TODO decide with Test_Isac *) |
518 fun is_atom t = length (vars t) = 1 |
518 fun is_atom t = length (vars t) = 1 |
519 fun is_atom (Const ("Float.Float",_) $ _) = true |
519 fun is_atom (Const ("Float.Float",_) $ _) = true |
520 | is_atom (Const ("ComplexI.I'_'_",_)) = true |
520 | is_atom (Const ("ComplexI.I'_'_",_)) = true |