1999-07-23 paulson 1999-07-23 now using correctly-typed constants from HOLogic
1999-07-23 paulson 1999-07-23 heavily revised by Jacques: coercions have alphabetic names; exponentiation is available, etc.
1999-07-23 paulson 1999-07-23 because intT is now defined in HOLogic
1999-07-23 paulson 1999-07-23 zmult_ac are no longer included by default
1999-07-23 paulson 1999-07-23 zadd_ac and zmult_ac are no longer included by default
1999-07-23 paulson 1999-07-23 added boolean and binary constants
1999-07-23 paulson 1999-07-23 new simprocs assoc_fold and combine_coeff
1999-07-23 wenzelm 1999-07-23 rail -a;
1999-07-23 wenzelm 1999-07-23 tuned add_term_varnames;
1999-07-23 wenzelm 1999-07-23 replaced assoc lists by Symtab.table;
1999-07-23 wenzelm 1999-07-23 Type.norm_term;
1999-07-23 wenzelm 1999-07-23 replace assoc lists by Symtab.table;
1999-07-23 wenzelm 1999-07-23 require_thy: fixed performance leak;
1999-07-23 wenzelm 1999-07-23 fix occurences of numerals in HOL/ZF terms;
1999-07-23 nipkow 1999-07-23 New lemmas by Stefan Merz.
1999-07-22 wenzelm 1999-07-22 avoid '(0 subgoals)';
1999-07-22 wenzelm 1999-07-22 Toplevel.excursion_error;
1999-07-22 wenzelm 1999-07-22 added exists;
1999-07-22 berghofe 1999-07-22 Tuned.
1999-07-21 paulson 1999-07-21 a stronger diff_less and no more le_diff_less
1999-07-21 paulson 1999-07-21 removed 2 qed_goals
1999-07-21 paulson 1999-07-21 tweaked proofs to handle new freeness reasoning for data c onstructors
1999-07-21 paulson 1999-07-21 more existing theorems renamed to use #0; also new results
1999-07-21 paulson 1999-07-21 now exports mk_bin
1999-07-21 paulson 1999-07-21 a more robust proof
1999-07-21 paulson 1999-07-21 tweaked proof after removal of diff_is_0_eq RS iffD2
1999-07-21 paulson 1999-07-21 better error message for curried recdefs, etc.
1999-07-21 nipkow 1999-07-21 Mod by Norber Voelcker
1999-07-20 wenzelm 1999-07-20 checkpoint;
1999-07-20 berghofe 1999-07-20 Eliminated addDistinct.
1999-07-19 wenzelm 1999-07-19 facts: no statement_binds;
1999-07-19 berghofe 1999-07-19 Datatype package now handles arbitrarily branching datatypes.
1999-07-19 wenzelm 1999-07-19 skeleton only;
1999-07-19 wenzelm 1999-07-19 added isar-ref;
1999-07-19 berghofe 1999-07-19 Documented usage of function types in datatype specifications.
1999-07-19 wenzelm 1999-07-19 added attdx, methdx;
1999-07-19 wenzelm 1999-07-19 added isabelle_isar logo;
1999-07-19 wenzelm 1999-07-19 updated; tuned;
1999-07-19 wenzelm 1999-07-19 renamed 'with' to 'using';
1999-07-19 wenzelm 1999-07-19 *** empty log message ***
1999-07-19 paulson 1999-07-19 NatBin: binary arithmetic for the naturals
1999-07-19 paulson 1999-07-19 examples of arithmetic on the naturals
1999-07-19 paulson 1999-07-19 deleted a reference to "nat", now erroneous because "nat" is a function
1999-07-19 paulson 1999-07-19 many new laws about div and mod
1999-07-19 paulson 1999-07-19 new theorem zless_zero_nat
1999-07-19 paulson 1999-07-19 removal of rewrites for Suc(Suc(Suc...)))
1999-07-19 paulson 1999-07-19 NatBin: binary arithmetic for the naturals
1999-07-19 paulson 1999-07-19 getting rid of qed_goal
1999-07-19 paulson 1999-07-19 getting rid of qed_goal
1999-07-19 paulson 1999-07-19 new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
1999-07-18 nipkow 1999-07-18 Modifid length_tl
1999-07-16 wenzelm 1999-07-16 adapted to dest_keywords, dest_parsers;
1999-07-16 wenzelm 1999-07-16 separate command tokens;
1999-07-16 wenzelm 1999-07-16 tuned dest_lexicon;
1999-07-16 wenzelm 1999-07-16 tuned;
1999-07-16 wenzelm 1999-07-16 removed break;
1999-07-16 wenzelm 1999-07-16 removed BREAK, ROLLBACK;
1999-07-16 wenzelm 1999-07-16 structure LocalDefs = LocalDefs; structure Calculation = Calculation; structure SkipProof = SkipProof;
1999-07-16 berghofe 1999-07-16 Exported function unify_consts (workaround to avoid inconsistently typed recursive constants in inductive and primrec definitions).
1999-07-16 berghofe 1999-07-16 Added new example (infinitely branching trees).