2002-03-01 wenzelm 2002-03-01 clarified outer syntax;
2002-03-01 wenzelm 2002-03-01 option -S 180;
2002-03-01 wenzelm 2002-03-01 clarified -l option; tuned;
2002-03-01 wenzelm 2002-03-01 structure Typtab; clarified typ_ord; clarified compress_type;
2002-03-01 wenzelm 2002-03-01 tuned;
2002-03-01 wenzelm 2002-03-01 tuned;
2002-03-01 wenzelm 2002-03-01 tuned;
2002-03-01 prensani 2002-03-01 Completed annonce of HoareParallel
2002-03-01 wenzelm 2002-03-01 tuned;
2002-03-01 paulson 2002-03-01 some addresses
2002-03-01 paulson 2002-03-01 lcp's try
2002-03-01 wenzelm 2002-03-01 enable_interrupt is back!
2002-02-28 wenzelm 2002-02-28 tuned;
2002-02-28 wenzelm 2002-02-28 renamed mask_interrupt to ignore_interrupt; renamed exhibit_interrupt to raise_interrupt; fixed interrupt handling code (more correct use of continuation);
2002-02-28 wenzelm 2002-02-28 renamed mask_interrupt to ignore_interrupt; renamed exhibit_interrupt to raise_interrupt; tuned interrupt handling code;
2002-02-28 wenzelm 2002-02-28 renamed mask_interrupt to ignore_interrupt; renamed exhibit_interrupt to raise_interrupt;
2002-02-28 wenzelm 2002-02-28 use ignore_interrupt, raise_interrupt;
2002-02-28 wenzelm 2002-02-28 delete .cvsignore;
2002-02-28 wenzelm 2002-02-28 export THIS_IS_ISABELLE_ADMIN=true;
2002-02-28 wenzelm 2002-02-28 fixed date;
2002-02-28 wenzelm 2002-02-28 more stuff;
2002-02-28 wenzelm 2002-02-28 moved match_bvs, match_bvars, renAbs to term.ML;
2002-02-28 wenzelm 2002-02-28 added match_bvars, rename_abs (from thm.ML);
2002-02-28 wenzelm 2002-02-28 rewrite_term: Term.rename_abs;
2002-02-28 wenzelm 2002-02-28 decomp_simp': use lhs instead of elhs (preserves more bound variable names);
2002-02-28 kleing 2002-02-28 included LBVSpec again
2002-02-28 wenzelm 2002-02-28 updated;
2002-02-28 wenzelm 2002-02-28 contexts, locales, sym(metric);
2002-02-28 paulson 2002-02-28 fixing nat_combine_numerals simprocs (again) Theorem eq_cong2 moved from Integ/int_arith1.ML to simpdata.ML, where it will be available in all theories. Function simplify_meta_eq now makes the meta-equality first so that eq_cong2 will work properly.
2002-02-28 kleing 2002-02-28 enforce positive branch targets
2002-02-28 kleing 2002-02-28 fixed missing label
2002-02-28 kleing 2002-02-28 fixed document
2002-02-27 wenzelm 2002-02-27 tuned feedback of goal forms;
2002-02-27 wenzelm 2002-02-27 improved messages;
2002-02-27 wenzelm 2002-02-27 tuned local goal forms;
2002-02-27 wenzelm 2002-02-27 'declare': and_list1; 'obtain': updated;
2002-02-27 wenzelm 2002-02-27 tuned;
2002-02-27 wenzelm 2002-02-27 'using' command;
2002-02-27 wenzelm 2002-02-27 renamed 'uses' to 'includes';
2002-02-27 wenzelm 2002-02-27 tuned;
2002-02-27 schirmer 2002-02-27 Some simple properties of dynamic accessibility added.
2002-02-27 schirmer 2002-02-27 Cleaning up the definition of static overriding.
2002-02-26 wenzelm 2002-02-26 tuned;
2002-02-26 wenzelm 2002-02-26 quote "includes" (now a keyword);
2002-02-26 wenzelm 2002-02-26 clarified localized multi statements;
2002-02-26 wenzelm 2002-02-26 added smart_have_thmss (global storage); removed add_thmss_hybrid; clarified add_thmss;
2002-02-26 wenzelm 2002-02-26 clarified multi statements;
2002-02-26 wenzelm 2002-02-26 clarified general_statement syntax;
2002-02-26 wenzelm 2002-02-26 renamed "uses" to "includes";
2002-02-26 wenzelm 2002-02-26 updated;
2002-02-26 wenzelm 2002-02-26 markup commands: proper theory/proof transactions!
2002-02-26 wenzelm 2002-02-26 tuned long_statement;
2002-02-26 kleing 2002-02-26 introduces SystemClasses and BVExample
2002-02-26 nipkow 2002-02-26 *** empty log message ***
2002-02-26 paulson 2002-02-26 Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and return False for e.g. Suc x = 0. Removed ad-hoc lemmas for that purpose.
2002-02-26 nipkow 2002-02-26 *** empty log message ***
2002-02-26 nipkow 2002-02-26 *** empty log message ***
2002-02-26 wenzelm 2002-02-26 Isar_examples/W_correct moved to W0;
2002-02-26 wenzelm 2002-02-26 tuned;
2002-02-26 wenzelm 2002-02-26 converted;