2000-10-25 wenzelm 2000-10-25 more "xsymbols" syntax;
2000-10-25 wenzelm 2000-10-25 "List prefixes" library theory (replaces old Lex/Prefix);
2000-10-25 nipkow 2000-10-25 *** empty log message ***
2000-10-25 nipkow 2000-10-25 *** empty log message ***
2000-10-25 paulson 2000-10-25 inputs Even.tex
2000-10-25 paulson 2000-10-25 minor tinkering
2000-10-25 paulson 2000-10-25 Even numbers section of Inductive chapter
2000-10-25 wenzelm 2000-10-25 tuned msg;
2000-10-25 wenzelm 2000-10-25 antiquotation "goals": error message;
2000-10-24 wenzelm 2000-10-24 * support sub/super scripts (for single symbols only), input syntax is like this: "A\<^sup>*" or "A\<^sup>\<star>"; * antiquotation @{goals} for output of *dynamic* goals state; Note that presentation of goal states does not conform to actual human-readable proof documents. Please do not include goal states into document output unless you really know what you are doing!
2000-10-24 wenzelm 2000-10-24 let commands access Toplevel.state; added command "goals" and option "goals_limit";
2000-10-24 wenzelm 2000-10-24 added pretty_goals;
2000-10-24 wenzelm 2000-10-24 added antiquotation "goals" and option "goals_limit"; tuned;
2000-10-24 wenzelm 2000-10-24 tuned;
2000-10-24 wenzelm 2000-10-24 added clasimpset: unit -> clasimpset;
2000-10-24 wenzelm 2000-10-24 tuned;
2000-10-24 paulson 2000-10-24 Acc example
2000-10-24 paulson 2000-10-24 even numbers example
2000-10-23 wenzelm 2000-10-23 intro_classes by default; tuned;
2000-10-23 wenzelm 2000-10-23 declare trancl rules;
2000-10-23 wenzelm 2000-10-23 tuned;
2000-10-23 wenzelm 2000-10-23 updated;
2000-10-23 wenzelm 2000-10-23 intro_classes by default;
2000-10-23 wenzelm 2000-10-23 make sure default document works;
2000-10-23 wenzelm 2000-10-23 comment out Pure-copied target;
2000-10-23 wenzelm 2000-10-23 * HOL: default proof step now includes 'intro_classes';
2000-10-23 nipkow 2000-10-23 *** empty log message ***
2000-10-23 paulson 2000-10-23 part of set-up
2000-10-23 paulson 2000-10-23 sets chapter
2000-10-23 paulson 2000-10-23 fixed crossref
2000-10-23 paulson 2000-10-23 tidied
2000-10-23 paulson 2000-10-23 X-symbol
2000-10-23 paulson 2000-10-23 auto gen
2000-10-23 paulson 2000-10-23 addition of Rules, Sets and some macros of lcp
2000-10-23 paulson 2000-10-23 goodbye to this dummy file
2000-10-23 paulson 2000-10-23 now includes Rules, Sets (?)
2000-10-23 paulson 2000-10-23 the Rules chapter and theories
2000-10-23 paulson 2000-10-23 the Sets chapter and theories
2000-10-23 paulson 2000-10-23 quantifiers now allowed in inductive defs
2000-10-23 paulson 2000-10-23 tidied
2000-10-23 wenzelm 2000-10-23 isatool unsymbolize;
2000-10-23 wenzelm 2000-10-23 added type_definitionI;
2000-10-23 wenzelm 2000-10-23 tuned deps;
2000-10-23 paulson 2000-10-23 contrapos
2000-10-23 paulson 2000-10-23 two spelling fixes
2000-10-22 wenzelm 2000-10-22 tuned;
2000-10-22 wenzelm 2000-10-22 simplified quotients (only plain total equivs);
2000-10-20 wenzelm 2000-10-20 tuned;
2000-10-20 nipkow 2000-10-20 *** empty log message ***
2000-10-20 wenzelm 2000-10-20 tuned;
2000-10-20 nipkow 2000-10-20 *** empty log message ***
2000-10-19 wenzelm 2000-10-19 provide more theorems (see subset.thy); tuned;
2000-10-19 wenzelm 2000-10-19 InductAttrib;
2000-10-19 wenzelm 2000-10-19 improved typedef; tuned proofs;
2000-10-19 wenzelm 2000-10-19 improved typedef; tuned;
2000-10-19 wenzelm 2000-10-19 added theory for HOL type definitions;
2000-10-19 wenzelm 2000-10-19 tuned;
2000-10-19 wenzelm 2000-10-19 added Tools/induct_attrib.ML;
2000-10-19 wenzelm 2000-10-19 declare sym [elim?] in HOL.ML instead of Calculation.thy;
2000-10-19 wenzelm 2000-10-19 tuned \isasymuniqex;