1997-11-28 nipkow 1997-11-28 Removed dead code.
1997-11-28 nipkow 1997-11-28 Moved the quantifier elimination simp procs into Provers.
1997-11-28 nipkow 1997-11-28 Quantifier elimination procs.
1997-11-28 nipkow 1997-11-28 Fixed the definition of `termord': is now antisymmetric.
1997-11-27 wenzelm 1997-11-27 several minor updates;
1997-11-27 wenzelm 1997-11-27 SYNC;
1997-11-27 wenzelm 1997-11-27 removed read_cterms;
1997-11-27 wenzelm 1997-11-27 fixed warning;
1997-11-27 wenzelm 1997-11-27 removed same_thm;
1997-11-27 paulson 1997-11-27 Tidying, mostly indentation
1997-11-27 paulson 1997-11-27 Deleted some needless addSIs; got rid of a slow Blast_tac
1997-11-27 wenzelm 1997-11-27 mk_norm_sum;
1997-11-26 wenzelm 1997-11-26 separate lists of simprocs;
1997-11-26 paulson 1997-11-26 Added rule impCE'
1997-11-26 paulson 1997-11-26 Blast_tac can prove Pelletier\'s problem 46\!
1997-11-26 paulson 1997-11-26 Tidying and using equalityCE instead of the slower equalityE
1997-11-26 paulson 1997-11-26 The change from iffE to iffCE means fewer case splits in most cases. Very few proofs are affected, almost none adversely
1997-11-26 paulson 1997-11-26 Tidying
1997-11-26 paulson 1997-11-26 Tidying and modification to cope with iffCE
1997-11-26 paulson 1997-11-26 Added rule impCE'
1997-11-26 paulson 1997-11-26 Changes to AddIs improve performance of Blast_tac
1997-11-26 paulson 1997-11-26 Statistics
1997-11-26 paulson 1997-11-26 updated comment
1997-11-26 paulson 1997-11-26 Tidying and modification to cope with iffCE
1997-11-26 wenzelm 1997-11-26 added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
1997-11-26 wenzelm 1997-11-26 added Arith provers;
1997-11-26 wenzelm 1997-11-26 Setup various arithmetic proof procedures.
1997-11-26 wenzelm 1997-11-26 added dest_nat;
1997-11-26 wenzelm 1997-11-26 moved to Arith/;
1997-11-26 wenzelm 1997-11-26 Cancel common constant factor from balanced exression.
1997-11-26 wenzelm 1997-11-26 Cancel common summands of balanced expressions.
1997-11-26 wenzelm 1997-11-26 removed conv_prover;
1997-11-26 wenzelm 1997-11-26 tuned;
1997-11-26 wenzelm 1997-11-26 added crep_cterm;
1997-11-26 wenzelm 1997-11-26 fixed type of thms_containing;
1997-11-26 wenzelm 1997-11-26 added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a; added foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a; added foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a;
1997-11-26 wenzelm 1997-11-26 cleaned signature; added instantiate': ctyp option list -> cterm option list -> thm -> thm;
1997-11-26 wenzelm 1997-11-26 removed merge_opts;
1997-11-25 mueller 1997-11-25 managed merge details;
1997-11-25 mueller 1997-11-25 resolved merge conflict;
1997-11-24 nipkow 1997-11-24 Added read_def_cterms for simultaneous reading/typing of terms under defaults. Redefined read_def_cterm in in terms of read_def_cterms. Deleted obsolete read_cterms. Cleaned up def of read_insts, which is not much shorter but much clearere are correcter now.
1997-11-22 wenzelm 1997-11-22 fixed warning;
1997-11-22 wenzelm 1997-11-22 made SML/NJ happy;
1997-11-22 wenzelm 1997-11-22 tuned;
1997-11-21 wenzelm 1997-11-21 replaced by seq.ML;
1997-11-21 wenzelm 1997-11-21 changed Pure/Sequence interface;
1997-11-21 wenzelm 1997-11-21 SYNC;
1997-11-21 wenzelm 1997-11-21 cd, use: path variables;
1997-11-21 wenzelm 1997-11-21 comment;
1997-11-21 wenzelm 1997-11-21 obsolete;
1997-11-21 wenzelm 1997-11-21 changed Pure/Sequence interface -- isatool fixseq;
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-11-21 wenzelm 1997-11-21 cd, use etc. now support path variables; changed Pure/Sequence interface;
1997-11-21 wenzelm 1997-11-21 fix references to obsolete Pure/Sequence structure;
1997-11-21 paulson 1997-11-21 tidying
1997-11-21 paulson 1997-11-21 analz_mono_contra_tac was wrong
1997-11-21 paulson 1997-11-21 Deleted some useless comments
1997-11-21 oheimb 1997-11-21 minor improvements of formulation and proofs
1997-11-21 oheimb 1997-11-21 corrected INDUCT_FILES
1997-11-20 wenzelm 1997-11-20 $ISABELLE_HOME/src;