2001-12-14 wenzelm 2001-12-14 export add_tvarsT etc.;
2001-12-14 wenzelm 2001-12-14 changed Type.varify;
2001-12-14 wenzelm 2001-12-14 Term.invent_type_names;
2001-12-13 nipkow 2001-12-13 *** empty log message ***
2001-12-13 nipkow 2001-12-13 *** empty log message ***
2001-12-13 wenzelm 2001-12-13 made SML/XL happy;
2001-12-13 nipkow 2001-12-13 *** empty log message ***
2001-12-13 nipkow 2001-12-13 Terminator now uses arith_tac as well.
2001-12-13 nipkow 2001-12-13 comp -> rel_comp
2001-12-13 wenzelm 2001-12-13 isatool expandshort;
2001-12-13 paulson 2001-12-13 Relaxed the precondition of UN_upper_le
2001-12-12 wenzelm 2001-12-12 isatool expandshort;
2001-12-12 nipkow 2001-12-12 new rewrite rules for use by arith_tac to take care of uminus. mods due to reorienting and renaming of real_minus_mult_eq1/2
2001-12-12 nipkow 2001-12-12 new rewrite rules for use by arith_tac to take care of uminus.
2001-12-12 nipkow 2001-12-12 mods due to reorienting and renaming of real_minus_mult_eq1/2
2001-12-12 nipkow 2001-12-12 tuned conversion from terms to "polynomials" for arith_tac: takes care of "uminus" now.
2001-12-12 wenzelm 2001-12-12 drop_judgment: be graceful about undeclared judgment;
2001-12-12 wenzelm 2001-12-12 obsolete;
2001-12-12 wenzelm 2001-12-12 option "-d pdf" by default (accomodates pdf bias of Mac OS X); tuned getpwnam;
2001-12-12 wenzelm 2001-12-12 removed installfonts, xterm interface; improved default of PROOFGENERAL_OPTIONS;
2001-12-12 nipkow 2001-12-12 Removed pointless backtracking from arith_tac
2001-12-12 berghofe 2001-12-12 Improved error messages.
2001-12-12 nipkow 2001-12-12 *** empty log message ***
2001-12-11 wenzelm 2001-12-11 tuned;
2001-12-11 wenzelm 2001-12-11 obsolete;
2001-12-11 wenzelm 2001-12-11 obsolete;
2001-12-11 wenzelm 2001-12-11 tuned;
2001-12-11 wenzelm 2001-12-11 \isasymindex made text mode;
2001-12-11 wenzelm 2001-12-11 isatools "symbolinput" and "nonascii" have disappeared;
2001-12-11 wenzelm 2001-12-11 added HOL-Library;
2001-12-11 wenzelm 2001-12-11 tuned;
2001-12-11 wenzelm 2001-12-11 updated;
2001-12-11 wenzelm 2001-12-11 removed altogether;
2001-12-11 wenzelm 2001-12-11 removed unused stuff;
2001-12-11 berghofe 2001-12-11 Updated.
2001-12-11 wenzelm 2001-12-11 oops;
2001-12-10 wenzelm 2001-12-10 bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
2001-12-10 wenzelm 2001-12-10 updated reserved words of HOL;
2001-12-10 wenzelm 2001-12-10 * HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam" -- INCOMPATIBILITY;
2001-12-10 wenzelm 2001-12-10 obsolete;
2001-12-10 wenzelm 2001-12-10 removed additional blank line (confuses some versions of make);
2001-12-10 wenzelm 2001-12-10 obsolete;
2001-12-10 berghofe 2001-12-10 - Changed type of invoke_codegen - Added combinators for sequences
2001-12-10 berghofe 2001-12-10 - Added code generator interface for types - Changed type of invoke_codegen
2001-12-10 berghofe 2001-12-10 Fixed bug in function find_paths.
2001-12-10 berghofe 2001-12-10 Added example file for intuitionistic logic (taken from FOL).
2001-12-10 berghofe 2001-12-10 Added support for code generation.
2001-12-10 berghofe 2001-12-10 Recursive equations to be used for code generation are now registered via RecfunCodegen.add
2001-12-10 berghofe 2001-12-10 Code generator for recursive functions.
2001-12-10 berghofe 2001-12-10 Tuned header.
2001-12-10 berghofe 2001-12-10 Code generator for datatypes.
2001-12-10 berghofe 2001-12-10 Moved contents to files datatype_codegen.ML and recfun_codegen.ML
2001-12-10 berghofe 2001-12-10 Turned subcls1 into an inductive relation to make it executable.
2001-12-10 berghofe 2001-12-10 Example for code generator.
2001-12-10 berghofe 2001-12-10 Added examples for code generator.
2001-12-10 berghofe 2001-12-10 Added code generator setup.
2001-12-10 berghofe 2001-12-10 Tuned code generator setup.
2001-12-10 berghofe 2001-12-10 Added new files (code generator and examples).
2001-12-10 berghofe 2001-12-10 Moved code generator setup from Recdef to Inductive.
2001-12-10 berghofe 2001-12-10 Replaced several occurrences of "blast" by "rules".