2001-01-11 wenzelm 2001-01-11 added strict_prefixI', strict_prefixE';
2001-01-11 wenzelm 2001-01-11 subst syntax;
2001-01-11 nipkow 2001-01-11 *** empty log message ***
2001-01-11 paulson 2001-01-11 lcp's suggestions for CTL
2001-01-11 nipkow 2001-01-11 *** empty log message ***
2001-01-11 paulson 2001-01-11 a new label
2001-01-11 paulson 2001-01-11 revisions corresponding to the new version of sets.tex
2001-01-10 nipkow 2001-01-10 Added <cdot> syntax for continuous application $.
2001-01-10 wenzelm 2001-01-10 isatool unsymbolize;
2001-01-10 wenzelm 2001-01-10 updated;
2001-01-10 wenzelm 2001-01-10 tuned \DOT, \DDOT;
2001-01-10 wenzelm 2001-01-10 added \<wrong> symbol;
2001-01-10 wenzelm 2001-01-10 tuned;
2001-01-10 paulson 2001-01-10 revisions e.g. images, transitive closure...
2001-01-10 nipkow 2001-01-10 *** empty log message ***
2001-01-10 nipkow 2001-01-10 *** empty log message ***
2001-01-10 paulson 2001-01-10 case_tac on bools
2001-01-10 paulson 2001-01-10 case_tac subgoals
2001-01-10 paulson 2001-01-10 deleted the obsolete nat_neqE (and reformatting)
2001-01-10 paulson 2001-01-10 deleted the obsolete nat_neqE
2001-01-10 paulson 2001-01-10 generalizing the LEAST theorems from "nat" to linear orderings and wellorderings
2001-01-10 paulson 2001-01-10 now using "by" for one-line proofs
2001-01-10 paulson 2001-01-10 various changes including the SOME examples, rule_format and "by"
2001-01-10 paulson 2001-01-10 loads the new theory
2001-01-10 paulson 2001-01-10 reformatting, and splitting the end of "Primes" to create "Forward"
2001-01-10 nipkow 2001-01-10 *** empty log message ***
2001-01-10 paulson 2001-01-10 now using "by" for one-line proofs
2001-01-10 paulson 2001-01-10 introduction of "by" and a few examples of SOME
2001-01-10 paulson 2001-01-10 auto update
2001-01-10 paulson 2001-01-10 new wfrec example
2001-01-10 paulson 2001-01-10 fixed the treatment of Rules and Sets
2001-01-10 nipkow 2001-01-10 *** empty log message ***
2001-01-10 wenzelm 2001-01-10 use \<acute>;
2001-01-10 wenzelm 2001-01-10 added \<dieresis>, \<acute>, \<cedilla>, \<emptyset>;
2001-01-09 wenzelm 2001-01-09 added acute, cedilla, dieresis, hungarumlaut;
2001-01-09 nipkow 2001-01-09 ` -> $
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2001-01-09 nipkow 2001-01-09 `` -> ` and ``` -> ``
2001-01-09 nipkow 2001-01-09 `` -> and ``` -> ``
2001-01-09 wenzelm 2001-01-09 replaced \<macron> by \<inverse>;
2001-01-09 wenzelm 2001-01-09 avoid renaming of params in cases;
2001-01-09 wenzelm 2001-01-09 split_all operation;
2001-01-09 oheimb 2001-01-09 improved evaluation judgment syntax; modified Loop rule
2001-01-09 wenzelm 2001-01-09 syntax (xsymbols);
2001-01-08 nipkow 2001-01-08 Removed Applyall
2001-01-08 paulson 2001-01-08 additional pattern allows reduction of fractions to lowest terms
2001-01-08 nipkow 2001-01-08 *** empty log message ***
2001-01-07 wenzelm 2001-01-07 updated;
2001-01-07 wenzelm 2001-01-07 removed ID (avoid CVS conflicts with generated versions);
2001-01-07 wenzelm 2001-01-07 CHANGED_PROP;
2001-01-07 wenzelm 2001-01-07 removed MicroJava/BV/Convert.thy;
2001-01-07 wenzelm 2001-01-07 do not AutoBind.drop_judgment;
2001-01-07 wenzelm 2001-01-07 tuned output;
2001-01-07 wenzelm 2001-01-07 tuned norm_hhf(_tac);
2001-01-07 wenzelm 2001-01-07 added is_norm_hhf;
2001-01-07 wenzelm 2001-01-07 removed outdated comment;
2001-01-07 wenzelm 2001-01-07 case binds: AutoBind.drop_judgment;
2001-01-07 wenzelm 2001-01-07 tuned split_all_tac;
2001-01-07 kleing 2001-01-07 merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
2001-01-06 wenzelm 2001-01-06 support ?case binding; tuned;