61 "----------- sameFunId -------------------------------------------"; |
61 "----------- sameFunId -------------------------------------------"; |
62 "----------- sameFunId -------------------------------------------"; |
62 "----------- sameFunId -------------------------------------------"; |
63 "----------- sameFunId -------------------------------------------"; |
63 "----------- sameFunId -------------------------------------------"; |
64 val t = str2term "M_b L"; atomty t; |
64 val t = str2term "M_b L"; atomty t; |
65 val t as f1 $ _ = str2term "M_b L"; |
65 val t as f1 $ _ = str2term "M_b L"; |
66 val t as Const ("op =", _) $ (f2 $ _) $ _ = str2term "M_b x = c + L*x"; |
66 val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = str2term "M_b x = c + L*x"; |
67 f1 = f2 (*true*); |
67 f1 = f2 (*true*); |
68 val (p as Const ("Atools.sameFunId",_) $ |
68 val (p as Const ("Atools.sameFunId",_) $ |
69 (f1 $ _) $ |
69 (f1 $ _) $ |
70 (Const ("op =", _) $ (f2 $ _) $ _)) = |
70 (Const ("HOL.eq", _) $ (f2 $ _) $ _)) = |
71 str2term "sameFunId (M_b L) (M_b x = c + L*x)"; |
71 str2term "sameFunId (M_b L) (M_b x = c + L*x)"; |
72 f1 = f2 (*true*); |
72 f1 = f2 (*true*); |
73 eval_sameFunId "" "Atools.sameFunId" |
73 eval_sameFunId "" "Atools.sameFunId" |
74 (str2term "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*); |
74 (str2term "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*); |
75 eval_sameFunId "" "Atools.sameFunId" |
75 eval_sameFunId "" "Atools.sameFunId" |