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
1997-04-14 wenzelm 1997-04-14 no longer includes ~/.emacs;
1997-04-13 wenzelm 1997-04-13 fixed file name;
1997-04-13 wenzelm 1997-04-13 GENERATED TEXT;
1997-04-13 wenzelm 1997-04-13 tuned format;
1997-04-13 wenzelm 1997-04-13 GENERATED TEXT;
1997-04-13 wenzelm 1997-04-13 GENERATED TEXT;
1997-04-13 wenzelm 1997-04-13 fixencoding - fix references to isabelle font encoding;
1997-04-12 wenzelm 1997-04-12 tuned comments;
1997-04-12 wenzelm 1997-04-12 misc improvement;
1997-04-12 wenzelm 1997-04-12 Setup GNU Emacs for Isabelle environment.
1997-04-12 wenzelm 1997-04-12 tuned;
1997-04-11 wenzelm 1997-04-11 fixed { ... } shell syntax to accomodate bash 2.x;
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-04-11 wenzelm 1997-04-11 tuned error msg;
1997-04-10 paulson 1997-04-10 Updated discussion and references for inductive definitions
1997-04-10 nipkow 1997-04-10 Deleted stupid proof at the end not needed anywhere.
1997-04-10 nipkow 1997-04-10 Mod because of "Turned Addsimps into AddIffs for datatype laws."
1997-04-10 nipkow 1997-04-10 Turned Addsimps into AddIffs for datatype laws.
1997-04-10 paulson 1997-04-10 Changed some fast_tac to blast_tac
1997-04-10 nipkow 1997-04-10 Added trace output and replaced fast_tac set_cs by Fast_tac.
1997-04-09 oheimb 1997-04-09 replaced 'addwrapper' and 'addWrapper' by correct 'compwrapper' and 'compWrapper'
1997-04-09 nipkow 1997-04-09 Thorough update.
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-04-09 paulson 1997-04-09 Control over excessive branching by applying a log2 penalty Incorporation of debugging features Allows backtracking over haz rules if alternatives exist Subsitution for equality may more a rule from the haz to the safe part
1997-04-09 paulson 1997-04-09 Explicit depth bounds seem necessary
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-04-09 paulson 1997-04-09 Dependency on Provers/nat_transitive
1997-04-08 nipkow 1997-04-08 Couldn't solve n < n+1 because of missing -1
1997-04-08 nipkow 1997-04-08 Dep. on Provers/nat_transitive
1997-04-07 wenzelm 1997-04-07 added -t (run tests) option;
1997-04-04 wenzelm 1997-04-04 added -g, -h options; replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;
1997-04-04 wenzelm 1997-04-04 tuned xdvi invocation;
1997-04-04 wenzelm 1997-04-04 replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;
1997-04-04 wenzelm 1997-04-04 improved messages;
1997-04-04 wenzelm 1997-04-04 fixed diagnostic output of print modes;
1997-04-04 nipkow 1997-04-04 moved inj and surj from Set to Fun and Inv -> inv.
1997-04-04 nipkow 1997-04-04 Inv -> inv
1997-04-04 slotosch 1997-04-04 *** empty log message ***
1997-04-04 slotosch 1997-04-04 Added Example Quot CVS ----------------------------------------------------------------------
1997-04-04 slotosch 1997-04-04 Start Example
1997-04-04 nipkow 1997-04-04 inv -> inverse
1997-04-04 slotosch 1997-04-04 Example for higher order quotients: Fractionals