2006-08-17 haftmann 2006-08-17 dropped definitions_of
2006-08-17 haftmann 2006-08-17 added all_super_classes
2006-08-17 haftmann 2006-08-17 renamed module to thyname
2006-08-17 haftmann 2006-08-17 cleanup
2006-08-16 urbanc 2006-08-16 added missing supp_nat lemma
2006-08-14 haftmann 2006-08-14 added
2006-08-14 haftmann 2006-08-14 module restructuring
2006-08-14 haftmann 2006-08-14 code cleanup, instance_subsort now working
2006-08-14 haftmann 2006-08-14 added code generator packages
2006-08-14 haftmann 2006-08-14 adaptions to improvements
2006-08-14 haftmann 2006-08-14 added add_hook_bootstrap
2006-08-14 haftmann 2006-08-14 added new files
2006-08-14 haftmann 2006-08-14 simplified code generator setup
2006-08-14 haftmann 2006-08-14 added passage on class package
2006-08-14 haftmann 2006-08-14 updated code generator keywords
2006-08-14 berghofe 2006-08-14 Removed non-trivial definitions from calc_atm theorem list.
2006-08-14 berghofe 2006-08-14 Finished implementation of uniqueness proof for recursion combinator.
2006-08-14 chaieb 2006-08-14 *** empty log message ***
2006-08-14 chaieb 2006-08-14 Reification now handels binders.
2006-08-09 paulson 2006-08-09 consistent prefixing for skolem functions
2006-08-09 paulson 2006-08-09 blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
2006-08-09 webertj 2006-08-09 tuned: string_of_list, string_of_pair
2006-08-09 wenzelm 2006-08-09 * ProofContext.prems_limit is now -1 by default;
2006-08-09 wenzelm 2006-08-09 tuned proofs;
2006-08-09 wenzelm 2006-08-09 global goals/qeds: after_qed operates on Proof.context (potentially local_theory); tuned after_qeds;
2006-08-09 wenzelm 2006-08-09 renamed map_theory to theory; added theory_result; prems_limit: default ~1;
2006-08-09 wenzelm 2006-08-09 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;
2006-08-09 wenzelm 2006-08-09 locale interpretation command: after_qed;
2006-08-09 wenzelm 2006-08-09 int_option: signed_string_of_int;
2006-08-09 wenzelm 2006-08-09 global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
2006-08-08 paulson 2006-08-08 skolem declarations for built-in theorems
2006-08-08 paulson 2006-08-08 more explict variable names
2006-08-08 paulson 2006-08-08 tidying
2006-08-08 berghofe 2006-08-08 Adapted to older logfiles containing no cpu time.
2006-08-08 haftmann 2006-08-08 added code_constname keyword
2006-08-08 haftmann 2006-08-08 fixed code generator theorem generation
2006-08-08 haftmann 2006-08-08 improvements for 2nd codegenerator
2006-08-08 haftmann 2006-08-08 cleanup code generation for Numerals
2006-08-08 haftmann 2006-08-08 improved & fixed code generator theorem generation
2006-08-08 haftmann 2006-08-08 code generator refinements
2006-08-08 haftmann 2006-08-08 adding code lemma now works as expected
2006-08-08 haftmann 2006-08-08 added more examples
2006-08-08 haftmann 2006-08-08 dropped duplicated line
2006-08-08 haftmann 2006-08-08 added Tools/typedef_codegen.ML
2006-08-08 haftmann 2006-08-08 abandoned equal_list in favor for eq_list
2006-08-07 berghofe 2006-08-07 Simple ML script for producing Gnuplot files from isatest log files.
2006-08-07 webertj 2006-08-07 title fixed
2006-08-05 wenzelm 2006-08-05 updated;
2006-08-05 wenzelm 2006-08-05 avoid low-level tsig;
2006-08-05 wenzelm 2006-08-05 reworked read_instantiate -- separate read_insts;
2006-08-05 wenzelm 2006-08-05 tuned;
2006-08-05 wenzelm 2006-08-05 removed obsolete sign_of;
2006-08-05 wenzelm 2006-08-05 Amine Chaieb: experimental generic reflection and reification in HOL;
2006-08-05 isatest 2006-08-05 use atbroy101 instead of atbroy98 (freezes up)
2006-08-04 krauss 2006-08-04 Added Keywords: "otherwise" and "sequential", needed for function package's sequential mode.
2006-08-04 chaieb 2006-08-04 *** empty log message ***
2006-08-03 wenzelm 2006-08-03 Rule instantiations -- operations within a rule/subgoal context.
2006-08-03 wenzelm 2006-08-03 moved bires_inst_tac etc. to rule_insts.ML;
2006-08-03 wenzelm 2006-08-03 moved read_instantiate etc. to rule_insts.ML;
2006-08-03 wenzelm 2006-08-03 added Isar/rule_insts.ML;