equal
deleted
inserted
replaced
344 |
344 |
345 |
345 |
346 "---------fun eval_sameFunId -------------------------------------------------------------------"; |
346 "---------fun eval_sameFunId -------------------------------------------------------------------"; |
347 "---------fun eval_sameFunId -------------------------------------------------------------------"; |
347 "---------fun eval_sameFunId -------------------------------------------------------------------"; |
348 "---------fun eval_sameFunId -------------------------------------------------------------------"; |
348 "---------fun eval_sameFunId -------------------------------------------------------------------"; |
349 val t = @{term "M_b L"}; TermC.atomty t; |
349 val t = @{term "M_b L"}; TermC.atom_trace_detail @{context} t; |
350 val t as f1 $ _ = @{term "M_b L"}; |
350 val t as f1 $ _ = @{term "M_b L"}; |
351 val t as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"}; |
351 val t as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"}; |
352 f1 = f2 (*true*); |
352 f1 = f2 (*true*); |
353 val (p as Const (\<^const_name>\<open>sameFunId\<close>, _) $ |
353 val (p as Const (\<^const_name>\<open>sameFunId\<close>, _) $ |
354 (f1 $ _) $ |
354 (f1 $ _) $ |