equal
deleted
inserted
replaced
21 val thy = Atools.thy; |
21 val thy = Atools.thy; |
22 |
22 |
23 "----------- occurs_in -------------------------------------------"; |
23 "----------- occurs_in -------------------------------------------"; |
24 "----------- occurs_in -------------------------------------------"; |
24 "----------- occurs_in -------------------------------------------"; |
25 "----------- occurs_in -------------------------------------------"; |
25 "----------- occurs_in -------------------------------------------"; |
26 fun str2t str = (term_of o the o (parse thy )) str; |
26 fun str2term str = (term_of o the o (parse thy )) str; |
27 fun term2s t = Sign.string_of_term (sign_of thy) t; |
27 fun term2s t = Sign.string_of_term (sign_of thy) t; |
28 val t = str2t "x"; |
28 val t = str2term "x"; |
29 if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f"; |
29 if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f"; |
30 |
30 |
31 val t = str2term "x occurs_in x"; |
31 val t = str2term "x occurs_in x"; |
32 val Some (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0; |
32 val Some (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0; |
33 if (term2s t') = "x occurs_in x = True" then () |
33 if (term2s t') = "x occurs_in x = True" then () |
51 |
51 |
52 |
52 |
53 "----------- argument_of -----------------------------------------"; |
53 "----------- argument_of -----------------------------------------"; |
54 "----------- argument_of -----------------------------------------"; |
54 "----------- argument_of -----------------------------------------"; |
55 "----------- argument_of -----------------------------------------"; |
55 "----------- argument_of -----------------------------------------"; |
56 val t = str2t "argument_in (M_b x)"; |
56 val t = str2term "argument_in (M_b x)"; |
57 val Some (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0; |
57 val Some (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0; |
58 if term2s t' = "(argument_in M_b x) = x" then () |
58 if term2s t' = "(argument_in M_b x) = x" then () |
59 else raise error "atools.sml:(argument_in M_b x) = x ???"; |
59 else raise error "atools.sml:(argument_in M_b x) = x ???"; |
60 |
60 |
61 "----------- sameFunId -------------------------------------------"; |
61 "----------- sameFunId -------------------------------------------"; |