1997-04-22 wenzelm 1997-04-22 removed -norc;
1997-04-22 wenzelm 1997-04-22 tuned;
1997-04-21 nipkow 1997-04-21 Modified credits.
1997-04-21 paulson 1997-04-21 New elimination rule for "unique existence"
1997-04-21 paulson 1997-04-21 New introduction rule for "unique existence"
1997-04-21 paulson 1997-04-21 Reorganized under headings. Also documented Blast_tac and LFilter
1997-04-21 paulson 1997-04-21 Tidied up the indentation
1997-04-21 paulson 1997-04-21 Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
1997-04-21 paulson 1997-04-21 Penalty for branching instantiations reduced from log3 to log4. Now allows a branch to close by unifying an OConst with a Const.
1997-04-21 paulson 1997-04-21 New blast_tac demo
1997-04-21 paulson 1997-04-21 Without the type constraint, the inner equality was NOT a biconditional...
1997-04-21 paulson 1997-04-21 Now faster without calling Blast.depth_tac
1997-04-21 paulson 1997-04-21 Disabled the attempts for mutual induction to work so that single induction involving sum types can work
1997-04-18 nipkow 1997-04-18 Tuple patterns are allowed now in `case'
1997-04-18 nipkow 1997-04-18 *** empty log message ***
1997-04-18 wenzelm 1997-04-18 print_goals: fixed show_sorts semantics;
1997-04-18 wenzelm 1997-04-18 tuned check_has_sort; fixed norm_typ: also does norm_sort;
1997-04-18 wenzelm 1997-04-18 removed least_sort; added of_sort;
1997-04-18 wenzelm 1997-04-18 tuned err msg;
1997-04-18 paulson 1997-04-18 Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
1997-04-18 paulson 1997-04-18 Now loads theory LList indirectly: via LFilter
1997-04-18 paulson 1997-04-18 Now uses some "case" syntax (but could use more)
1997-04-18 paulson 1997-04-18 New monotonicity theorems
1997-04-18 paulson 1997-04-18 New theory: a corecursive filter functional
1997-04-18 paulson 1997-04-18 Removed needless parentheses from translation
1997-04-18 paulson 1997-04-18 ex/LFilter is a new theory (and dependency)
1997-04-18 paulson 1997-04-18 Automatic update
1997-04-17 wenzelm 1997-04-17 tuned error msgs;
1997-04-17 wenzelm 1997-04-17 improved type check error messages;
1997-04-17 wenzelm 1997-04-17 renamed set_ap to setmp;
1997-04-17 paulson 1997-04-17 Automatic updates
1997-04-17 paulson 1997-04-17 Removed the \date{} command in order to put the date of typesetting on the title page
1997-04-17 paulson 1997-04-17 Corrected the informal description of coinductive definition
1997-04-17 paulson 1997-04-17 Corrected the informal description of coinductive definition in sections 1 and 4.3, introducing the notion of "consistent with" a set of rules. Final version for Milner Festschrift?
1997-04-17 nipkow 1997-04-17 Added ability to have case expressions involving tuples. (via translation)
1997-04-17 wenzelm 1997-04-17 tuned;
1997-04-17 wenzelm 1997-04-17 *** empty log message ***
1997-04-17 wenzelm 1997-04-17 added fixencoding note;
1997-04-17 wenzelm 1997-04-17 fixed ISAMODE_HOME;
1997-04-17 wenzelm 1997-04-17 eliminated PLATFORM;
1997-04-16 wenzelm 1997-04-16 removed lceil, rceil, lfloor, rfloor;
1997-04-16 wenzelm 1997-04-16 fixed perl path (for sunbroys);
1997-04-16 wenzelm 1997-04-16 improved translations for subset symbols syntax: constraints;
1997-04-16 wenzelm 1997-04-16 moved classes / sorts to sorts.ML; moved (and reimplemented) type inference to type_infer.ML; cleaned up type unification; misc cleanup and tuning;
1997-04-16 wenzelm 1997-04-16 renamed subclass to classrel; tune type checking error msgs;
1997-04-16 wenzelm 1997-04-16 Sorts.str_of_sort;
1997-04-16 wenzelm 1997-04-16 Sorts.str_of_arity;
1997-04-16 wenzelm 1997-04-16 added sorts.ML, type_infer.ML;
1997-04-16 wenzelm 1997-04-16 tuned type of eq_ix, mem_ix;
1997-04-16 wenzelm 1997-04-16 improved inc, dec; added set_ap;
1997-04-16 wenzelm 1997-04-16 Type inference (isolated from type.ML, completely reimplemented).
1997-04-16 wenzelm 1997-04-16 Type classes and sorts (isolated from type.ML).
1997-04-16 wenzelm 1997-04-16 improved;
1997-04-15 paulson 1997-04-15 Partially converted to call blast_tac
1997-04-15 paulson 1997-04-15 Addition of blast_tac benchmark
1997-04-15 paulson 1997-04-15 Changed penalty from log2 to log3
1997-04-15 paulson 1997-04-15 An extra call to blast_tac (illustrating a need for type instantiation)
1997-04-15 paulson 1997-04-15 Now puts basic rewrites for lappend & lmap into the simpset
1997-04-15 paulson 1997-04-15 Removed "AddSDs [Scons_inject];" because (a) IT WAS WRONG (should have been AddSEs) (b) It was redundant (due to the AddIffs [...,Scons_Scons_eq])
1997-04-15 paulson 1997-04-15 Moved expand_case_tac from Auth/Message.ML to simpdata.ML