formal lcm definition for polynomials

moved lemmas out of Int.thy which have nothing to do with int

redundant: dropped

tuned Heap_Monad.successE

documentation

fixed a few mistakes in the documentation

tuning

'moura' method is also useful for reconstructing skolemization of lambda-lifting of formulas for other provers than Z3

actually finish after closing, e.g. relevant for consecutive (**)(**);

tuned

tuned;

tuned

don't call 'hd' on a possibly empty list

proper types for applied variables, for typed formats (TFF0, DFG)

don't affect other subgoals with 'auto' in one-liner proofs

tuned output in case of one-liner failure

updated docs with two provers: veriT and Zipperposition

give more facts to veriT -- it seems to be able to cope with them

use native encoding with Vampire -- modern versions handle types better than the old ones

always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')

correct inlining in veriT's subproofs.

repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'

tuning

tuning

keep rules with no premises in Isar proofs from veriT

correct indexing in the presence of lambda-lifting

merged

tuned

merge

support hypotheses with schematics in Isar proofs

tuned

simplified and repaired veriT index handling code