fixed bug in sortlookup

more concise preprocessing of numerals for code generation

more concise string serialization

added some codegen examples/applications

adapted using the characteristic equations

modified to use the characteristic equations

- Fixed bug that caused uniqueness proof for recursion combinator to fail for mutually recursive datatypes - Implemented proofs of characteristic equations for recursion combinator.

used the recursion combinator for the height and substitution function

added definition for size and substitution using the recursion combinator

improved thmtab

fixed bug in sortcontext extraction

dropped definitions_of

added all_super_classes

renamed module to thyname

cleanup

added missing supp_nat lemma

added

module restructuring

code cleanup, instance_subsort now working

added code generator packages

adaptions to improvements

added add_hook_bootstrap

added new files

simplified code generator setup

added passage on class package

updated code generator keywords

Removed non-trivial definitions from calc_atm theorem list.

Finished implementation of uniqueness proof for recursion combinator.

*** empty log message ***

Reification now handels binders.

consistent prefixing for skolem functions

blacklist augmented to block some "unit" theorems that cause unsound resolution proofs

tuned: string_of_list, string_of_pair

* ProofContext.prems_limit is now -1 by default;

tuned proofs;

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

renamed map_theory to theory; added theory_result; prems_limit: default ~1;

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 ***

Rule instantiations -- operations within a rule/subgoal context.

moved bires_inst_tac etc. to rule_insts.ML;

moved read_instantiate etc. to rule_insts.ML;

added Isar/rule_insts.ML;

removed obsolete commute, map_list;

removed obsolete add_term_tvarnames;

tuned;

tuned types_sorts, add_used;

RuleInsts.bires_inst_tac;

*** empty log message ***

fixed generator

added HOL/ex/Reflection;

removed True_implies (cf. True_implies_equals); added header;

removed OldGoals.legacy flag (always warn); added warning for legacy ML scripts;

removed OldGoals.legacy flag (always warn);

tuned;

removed True_implies (cf. True_implies_equals);

Generic reflection and reification (by Amine Chaieb).

Restructured algebra library, added ideals and quotient rings.

Updated comments.

updated;

tuned proofs;

lemma da_good_approx: adapted induction (was exploting lifted obtain result);

renamed Syntax.indexname to Syntax.read_indexname; added read_int (not Int.fromString, which admits ~ syntax of ML);

tuned;

moved debug option to proof_display.ML (again); normalized Proof.context/method type aliases;

normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export; prems_limit: < 0 means no output; added debug option (back from proof_display.ML);

simplified Assumption/ProofContext.export; simplified end_block;

added tactical result; simplified obtain_export: no Seq.seq, no lifting of result prems; tuned;

removed obsolete Drule.frees/vars_of etc.; simplified Assumption/ProofContext.export;

normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export;

simplified Proof.end_block;

removed obsolete Drule.frees/vars_of etc.; tuned;

normalized Proof.context/method type aliases; added declare/export/import_prf; added focus_subgoal: reset/declare goal schematics;

renamed Syntax.indexname to Syntax.read_indexname;

Variable.focus_subgoal;

replaced maxidx_of_proof by maxidx_proof;

prems-limit: int_option;

removed obsolete frees/vars_of etc.; removed obsolete freeze_all etc.; added norm_hhf_cterm; tuned fold_terms; renamed Syntax.indexname to Syntax.read_indexname;

fake predeclaration of type Proof.context;

simplified export: no Seq.seq; normalized Proof.context/method type aliases;

use proper RecdefPackage.get_hints; tuned;

removed obsolete Drule.frees/vars_of; renamed thm_vars to thm_varnames;

renamed thm_vars to thm_varnames;

removed obsolete Drule.freeze_all -- now uses legacy Drule.freeze_thaw;

export get_hints; tuned;

normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export; tuned;

normalized Proof.context/method type aliases;

simplified Assumption/ProofContext.export;

replaced obsolete standard/freeze_all by Variable.trade;

removed obsolete Drule.frees/vars_of etc.;

Added type constraint to please sml/nj

deleted obsolete file