Tue, 09 Jan 2001 15:15:28 +0100 wenzelm split_all operation;
Tue, 09 Jan 2001 13:54:44 +0100 oheimb improved evaluation judgment syntax; modified Loop rule
Tue, 09 Jan 2001 12:11:56 +0100 wenzelm syntax (xsymbols);
Mon, 08 Jan 2001 12:27:36 +0100 nipkow Removed Applyall
Mon, 08 Jan 2001 11:06:24 +0100 paulson additional pattern allows reduction of fractions to lowest terms
Mon, 08 Jan 2001 10:33:51 +0100 nipkow *** empty log message ***
Sun, 07 Jan 2001 22:39:28 +0100 wenzelm updated;
Sun, 07 Jan 2001 21:45:14 +0100 wenzelm removed ID (avoid CVS conflicts with generated versions);
Sun, 07 Jan 2001 21:41:56 +0100 wenzelm CHANGED_PROP;
Sun, 07 Jan 2001 21:40:49 +0100 wenzelm removed MicroJava/BV/Convert.thy;
Sun, 07 Jan 2001 21:37:40 +0100 wenzelm do not AutoBind.drop_judgment;
Sun, 07 Jan 2001 21:36:59 +0100 wenzelm tuned output;
Sun, 07 Jan 2001 21:36:11 +0100 wenzelm tuned norm_hhf(_tac);
Sun, 07 Jan 2001 21:35:34 +0100 wenzelm added is_norm_hhf;
Sun, 07 Jan 2001 21:35:11 +0100 wenzelm removed outdated comment;
Sun, 07 Jan 2001 21:34:45 +0100 wenzelm case binds: AutoBind.drop_judgment;
Sun, 07 Jan 2001 21:34:16 +0100 wenzelm tuned split_all_tac;
Sun, 07 Jan 2001 18:43:13 +0100 kleing merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
Sat, 06 Jan 2001 21:31:37 +0100 wenzelm support ?case binding;
Sat, 06 Jan 2001 21:31:09 +0100 wenzelm apply_case: more robust handling of bounds;
Sat, 06 Jan 2001 21:29:29 +0100 wenzelm moved norm_hhf_tac to Pure/tactic.ML;
Sat, 06 Jan 2001 21:28:30 +0100 wenzelm added drop_judgment;
Sat, 06 Jan 2001 21:28:04 +0100 wenzelm export read_inst', inst';
Sat, 06 Jan 2001 21:27:33 +0100 wenzelm added list_abs;
Sat, 06 Jan 2001 21:27:12 +0100 wenzelm added norm_hhf(_tac);
Sat, 06 Jan 2001 21:26:27 +0100 wenzelm Tactic.norm_hhf;
Sat, 06 Jan 2001 21:26:13 +0100 wenzelm 'of:' params spec;
Sat, 06 Jan 2001 21:22:35 +0100 wenzelm 'cases' / 'induct' method: ?case binding, 'of:' spec;
Sat, 06 Jan 2001 12:39:05 +0100 nipkow *** empty log message ***
Sat, 06 Jan 2001 11:27:09 +0100 nipkow *** empty log message ***
Sat, 06 Jan 2001 10:36:19 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 18:49:16 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 18:48:18 +0100 nipkow ^^ -> ```
Fri, 05 Jan 2001 18:33:47 +0100 paulson Fleuriot reference
Fri, 05 Jan 2001 18:32:57 +0100 paulson minor edits to Chapters 1-3
Fri, 05 Jan 2001 18:32:33 +0100 paulson revisions especially concerning the reals
Fri, 05 Jan 2001 18:31:48 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 18:16:01 +0100 paulson a few extra brackets
Fri, 05 Jan 2001 15:39:34 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 15:16:40 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 14:28:10 +0100 nipkow Changed priority of dvd from 70 to 50 as befits a relation.
Fri, 05 Jan 2001 13:10:37 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 10:19:32 +0100 paulson new UNITY examples by Sidi Ehmety
Fri, 05 Jan 2001 10:19:14 +0100 paulson Field of a relation, and some Domain/Range rules
Fri, 05 Jan 2001 10:18:46 +0100 paulson finite_trancl: new theorem by Sidi Ehmety
Fri, 05 Jan 2001 10:17:48 +0100 paulson more removal of obsolete rules
Fri, 05 Jan 2001 10:17:19 +0100 paulson fixed two proofs that were affected by the removal of obsolete rules
Fri, 05 Jan 2001 10:15:48 +0100 paulson new examples by Sidi Ehmety
Thu, 04 Jan 2001 19:41:13 +0100 wenzelm tuned comment;
Thu, 04 Jan 2001 19:39:53 +0100 wenzelm renamed .sml files to .ML;
Thu, 04 Jan 2001 18:13:27 +0100 nipkow label!
Thu, 04 Jan 2001 10:23:01 +0100 paulson more tidying, especially to remove real_of_posnat
Thu, 04 Jan 2001 10:22:33 +0100 paulson initial material on the Reals
Wed, 03 Jan 2001 21:27:15 +0100 wenzelm updated;
Wed, 03 Jan 2001 21:25:23 +0100 wenzelm added recdef_tc(_i);
Wed, 03 Jan 2001 21:24:29 +0100 wenzelm recdef_tc;
Wed, 03 Jan 2001 21:23:50 +0100 wenzelm renamed .sml files to .ML;
Wed, 03 Jan 2001 21:23:13 +0100 wenzelm TFL: renamed .sml to .ML;
Wed, 03 Jan 2001 21:22:37 +0100 wenzelm added 'recdef_tc' command;
Wed, 03 Jan 2001 21:21:28 +0100 wenzelm * Isar/HOL: added 'recdef_tc' command;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip