equal
deleted
inserted
replaced
306 | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
306 | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
307 | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
307 | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
308 | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) |
308 | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) |
309 | _ => (acc, dacc) |
309 | _ => (acc, dacc) |
310 val (cs,ds) = h ([],[]) p |
310 val (cs,ds) = h ([],[]) p |
311 val l = Integer.lcms (cs union ds) |
311 val l = Integer.lcms (gen_union (op =) (cs, ds)) |
312 fun cv k ct = |
312 fun cv k ct = |
313 let val (tm as b$s$t) = term_of ct |
313 let val (tm as b$s$t) = term_of ct |
314 in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t)) |
314 in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t)) |
315 |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end |
315 |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end |
316 fun nzprop x = |
316 fun nzprop x = |