2001-01-24 wenzelm 2001-01-24 * Document preparation: renamed standard symbols \<ll> to \<lless> and \<gg> to \<ggreater>;
2001-01-24 wenzelm 2001-01-24 added eufrak symbols; renamed \<ll> to \<lless> and \<gg> to \<ggreater>;
2001-01-24 wenzelm 2001-01-24 more symbols;
2001-01-24 wenzelm 2001-01-24 empty_upd_none;
2001-01-24 oheimb 2001-01-24 debugging and extensions
2001-01-24 nipkow 2001-01-24 *** empty log message ***
2001-01-24 nipkow 2001-01-24 *** empty log message ***
2001-01-24 wenzelm 2001-01-24 no_brackets;
2001-01-23 wenzelm 2001-01-23 tuned;
2001-01-23 paulson 2001-01-23 arg_cong, tacticals, pr, defer, prefer
2001-01-23 wenzelm 2001-01-23 added HOL-Unix example;
2001-01-23 paulson 2001-01-23 2 to #2
2001-01-23 paulson 2001-01-23 the 0<n premise was unnecessary
2001-01-23 paulson 2001-01-23 added a "pr" example; tidied
2001-01-22 paulson 2001-01-22 deleted several obsolete lemmas from NatArith.ML
2001-01-22 paulson 2001-01-22 tidied using arith_tac
2001-01-22 paulson 2001-01-22 deleted obsolete theorems
2001-01-22 paulson 2001-01-22 tided
2001-01-22 paulson 2001-01-22 arg_cong example; tidying to use @subgoals
2001-01-22 paulson 2001-01-22 rename_tac example; tidying to use @subgoals
2001-01-22 paulson 2001-01-22 new examples theory Rules/Tacticals.thy
2001-01-21 wenzelm 2001-01-21 setuo indent: \isaindent;
2001-01-21 wenzelm 2001-01-21 setup indent;
2001-01-21 wenzelm 2001-01-21 added spaces; added default_indent, indent;
2001-01-21 wenzelm 2001-01-21 support general indentation (e.g. for non-tt latex output); tuned;
2001-01-21 wenzelm 2001-01-21 added replicate_string;
2001-01-21 wenzelm 2001-01-21 updated;
2001-01-21 wenzelm 2001-01-21 \isaindent;
2001-01-20 wenzelm 2001-01-20 tuned;
2001-01-20 wenzelm 2001-01-20 Ring_and_Field_Example;
2001-01-20 wenzelm 2001-01-20 instance int :: ordered_ring moved to Ring_and_Field_Example, because it changes the way that int expressions get simplified, violating the strict library principle (cf. README.html);
2001-01-20 wenzelm 2001-01-20 added Library/Ring_and_Field_Example.thy;
2001-01-20 wenzelm 2001-01-20 *** empty log message ***
2001-01-19 wenzelm 2001-01-19 added HOL/Library/Nested_Environment.thy;
2001-01-19 wenzelm 2001-01-19 updated;
2001-01-19 wenzelm 2001-01-19 more bugs;
2001-01-19 wenzelm 2001-01-19 forget RPM;
2001-01-19 wenzelm 2001-01-19 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
2001-01-18 wenzelm 2001-01-18 made SML/XL happy;
2001-01-18 wenzelm 2001-01-18 tuned;
2001-01-18 wenzelm 2001-01-18 show(_i): check goal;
2001-01-18 wenzelm 2001-01-18 show/thus: check_goal;
2001-01-18 wenzelm 2001-01-18 show/thus: Toplevel.proof';
2001-01-18 wenzelm 2001-01-18 infix \\\\;
2001-01-18 wenzelm 2001-01-18 added exists_stamp; added PureN, CPureN;
2001-01-18 wenzelm 2001-01-18 use Sign.PureN, Sign.CPureN;
2001-01-18 wenzelm 2001-01-18 Sign.exists_stamp;
2001-01-18 wenzelm 2001-01-18 tuned \<And> and \<Or>;
2001-01-18 wenzelm 2001-01-18 generate index.html for pdf docs;
2001-01-18 oheimb 2001-01-18 splitted Loop rule
2001-01-18 paulson 2001-01-18 removed redundant proof
2001-01-18 oheimb 2001-01-18 is_class and class now as defs (rather than translations); corrected Digest.thy
2001-01-16 wenzelm 2001-01-16 use_output: proper handling of non-ASCII symbols;
2001-01-16 wenzelm 2001-01-16 export plain_output;
2001-01-16 kleing 2001-01-16 Store.thy is obsolete (newref isn't used any more)
2001-01-16 kleing 2001-01-16 removed obsolete MicroJava/JVM/Store.thy
2001-01-16 kleing 2001-01-16 newref -> new_Addr
2001-01-16 paulson 2001-01-16 renamings: real_of_nat, real_of_int -> (overloaded) real inf_close -> approx SReal -> Reals SNat -> Nats
2001-01-16 wenzelm 2001-01-16 renamed Product_Type.split to split_conv;
2001-01-16 wenzelm 2001-01-16 use Syntax.read_xnum;