moved all isatest/cron job related files to own directory

AnnoMaLy related files, as discussed in mails with Gerwin Klein

Simplify print mode. Support setproverflag.

Update test for new parse result

Add setproverflag, to replace other flag controls

Add objtypes to openblock/closeblock and theory items (can be used to control folding).

Add more attributes to openblock. Change theory item objtype field to proper objtype.

Add Isabelle-specific objtypes

Comment

clarified code

clarified error message

moved instance option :: finite to Finite_Set.thy

moved instance option :: finite here

Fix idvalue output and PGML print mode raw encode/decode.

permitting empty datatypes

improved handling of nat numerals

tuned code theorems for ord on integers

simplified code generator setup

tuned code theorems

added add_numerals_of

now using "class"

using "fst" "snd" for Haskell code

added code theorems for UNIV

adjusted to latest changes

new code theorems

syntax for "class attach const"

prefix of class interpretation not mandatory any longer

Meson.is_fol_term now takes a theory as argument. Minor tidying.

New code to store theorem names in a concise form rather than as fully-qualified. Meson.is_fol_term now takes a theory as argument.

The first-order test now tests for the obscure case of a polymorphic constant like 1 being used with a function type.

abbrev: be permissive after transformation;

exported get_ss, map_ss;

tuned;

tuned ML setup;

added @{const_name}, @{const_syntax};

more cleanup

Add closeblock/openblock structure to proof-block commands

Updated success string for Vampire. eprover no longer sought in the PROVER directory. eprover now gets tstp input. Streamlined the code a bit.

Now outputs metis calls

added headers

cleanup, fixing sml/nj related problems

gensym: removed bits of dead code;

gensym no longer includes ' or _ in names (trailing _ is bad)

tuned document;

\usepackage{amssymb};

moved some non-kernel material to more_thm.ML;

removed obsolete eq_set;

Thm.internalK;