equal
deleted
inserted
replaced
114 val t = term_of ct |
114 val t = term_of ct |
115 val xs = dest_binop_list cn t |
115 val xs = dest_binop_list cn t |
116 val js = subtract (op =) is (0 upto (length xs) - 1) |
116 val js = subtract (op =) is (0 upto (length xs) - 1) |
117 val ty = fastype_of t |
117 val ty = fastype_of t |
118 in |
118 in |
119 Goal.prove_internal [] |
119 Goal.prove_internal ctxt [] |
120 (cterm_of thy |
120 (cterm_of thy |
121 (Logic.mk_equals (t, |
121 (Logic.mk_equals (t, |
122 if null is |
122 if null is |
123 then mk (Const (neu, ty), foldr1 mk (map (nth xs) js)) |
123 then mk (Const (neu, ty), foldr1 mk (map (nth xs) js)) |
124 else if null js |
124 else if null js |