2003-02-07 nipkow 2003-02-07 (*f -> ( *f because of new comments
2003-02-07 nipkow 2003-02-07 Removed (*) because of comments
2003-02-07 nipkow 2003-02-07 Added (* ... *) comments in formulae.
2003-02-06 paulson 2003-02-06 changed ** to ## to avoid conflict with new comment syntax
2003-02-05 paulson 2003-02-05 more tidying
2003-02-04 paulson 2003-02-04 some x-symbols
2003-02-03 berghofe 2003-02-03 New tool for displaying version information.
2003-02-03 berghofe 2003-02-03 Fill in version information in lib/Tools/version.
2003-02-03 berghofe 2003-02-03 Added "print_intros" command.
2003-02-03 berghofe 2003-02-03 Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
2003-02-03 berghofe 2003-02-03 Moved find_intros_goal from goals.ML to pure_thy.ML
2003-02-03 berghofe 2003-02-03 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
2003-01-31 paulson 2003-01-31 conversion to new-style theories and tidying
2003-01-30 paulson 2003-01-30 conversion of UNITY theories to new-style
2003-01-30 paulson 2003-01-30 converting more UNITY theories to new-style
2003-01-29 berghofe 2003-01-29 Some tuning: - finite now uses rev_append (tail recursive!) to append stopper, because @ needs to much stack space for large strings - repeat is now tail recursive
2003-01-29 berghofe 2003-01-29 Added function rev_append.
2003-01-29 berghofe 2003-01-29 Fixed bug in function corr.
2003-01-29 paulson 2003-01-29 converted more UNITY theories to new-style
2003-01-29 nipkow 2003-01-29 *** empty log message ***
2003-01-29 paulson 2003-01-29 converting UNITY to new-style theories
2003-01-28 nipkow 2003-01-28 New example
2003-01-28 nipkow 2003-01-28 pos/neg_mod_sign/bound are now simp rules.
2003-01-27 kleing 2003-01-27 fixed missing UNITY files
2003-01-24 paulson 2003-01-24 More conversion of UNITY to Isar new-style theories
2003-01-24 paulson 2003-01-24 Partial conversion of UNITY to Isar new-style theories
2003-01-23 paulson 2003-01-23 tidying (by script)
2003-01-23 ballarin 2003-01-23 Fixed term order for normal form in rings.
2003-01-17 berghofe 2003-01-17 Added rename_abs attribute for renaming bound variables.
2003-01-17 nipkow 2003-01-17 *** empty log message ***
2003-01-15 paulson 2003-01-15 more new-style theories
2003-01-15 paulson 2003-01-15 moving "let" from ZF to FOL
2003-01-15 paulson 2003-01-15 auto-update
2003-01-09 nipkow 2003-01-09 *** empty log message ***
2003-01-08 nipkow 2003-01-08 New files in Hoare/
2003-01-08 oheimb 2003-01-08 corrected swallowing of newlines after end-of-ignore: rollback
2003-01-07 oheimb 2003-01-07 corrected swallowing of newlines after end-of-ignore (improved)
2003-01-07 nipkow 2003-01-07 new versions of merge-example
2003-01-06 nipkow 2003-01-06 Split Pointers.thy and automated one proof, which caused the runtime to explode
2003-01-05 nipkow 2003-01-05 *** empty log message ***
2003-01-03 nipkow 2003-01-03 *** empty log message ***
2002-12-30 nipkow 2002-12-30 *** empty log message ***
2002-12-29 nipkow 2002-12-29 *** empty log message ***
2002-12-29 nipkow 2002-12-29 *** empty log message ***
2002-12-29 nipkow 2002-12-29 *** empty log message ***
2002-12-23 nipkow 2002-12-23 *** empty log message ***
2002-12-22 nipkow 2002-12-22 removed some problems with print translations
2002-12-22 nipkow 2002-12-22 added print translations tha avoid eta contraction for important binders.
2002-12-22 nipkow 2002-12-22 *** empty log message ***
2002-12-20 nipkow 2002-12-20 *** empty log message ***
2002-12-19 paulson 2002-12-19 auto-update
2002-12-18 nipkow 2002-12-18 *** empty log message ***
2002-12-17 paulson 2002-12-17 auto-update
2002-12-17 paulson 2002-12-17 new int induction rules
2002-12-17 paulson 2002-12-17 new material for trace_unify_fail
2002-12-16 berghofe 2002-12-16 Added mk_int and mk_list.
2002-12-16 berghofe 2002-12-16 Code generator for datatypes now also generates suitable term_of functions (when term_of mode is switched on).
2002-12-16 berghofe 2002-12-16 - Added mode reference variable (may be used to switch on and off specific code generators), together with theory syntax - First steps towards reflection: added functions mk_type and mk_term_of
2002-12-13 oheimb 2002-12-13 cent/currency: changed from wasysym to textcomp because of PDF problems
2002-12-13 paulson 2002-12-13 trace_unify_fail