global goals/qeds: after_qed operates on Proof.context (potentially local_theory); theorem/interpretation: slightly more uniform treatment of after_qeds; theorem conclusion: proper fix_frees;

locale interpretation command: after_qed;

int_option: signed_string_of_int;

global goals/qeds: after_qed operates on Proof.context (potentially local_theory);

skolem declarations for built-in theorems

more explict variable names

tidying

Adapted to older logfiles containing no cpu time.

added code_constname keyword

fixed code generator theorem generation

improvements for 2nd codegenerator

cleanup code generation for Numerals

improved & fixed code generator theorem generation

code generator refinements

adding code lemma now works as expected

added more examples

dropped duplicated line

added Tools/typedef_codegen.ML

abandoned equal_list in favor for eq_list

Simple ML script for producing Gnuplot files from isatest log files.

title fixed

updated;

avoid low-level tsig;

reworked read_instantiate -- separate read_insts;

tuned;

removed obsolete sign_of;

Amine Chaieb: experimental generic reflection and reification in HOL;

use atbroy101 instead of atbroy98 (freezes up)

Added Keywords: "otherwise" and "sequential", needed for function package's sequential mode.

*** empty log message ***