Fri, 10 Nov 2000 19:00:22 +0100 wenzelm val atomize = thms "atomize'";
Fri, 10 Nov 2000 16:31:28 +0100 nipkow > etc
Fri, 10 Nov 2000 16:26:44 +0100 nipkow new: > and >=
Fri, 10 Nov 2000 15:05:09 +0100 nipkow rule inversion
Fri, 10 Nov 2000 09:17:54 +0100 nipkow JMB -> JMPB. Email von Johannes Pfeifroth.
Thu, 09 Nov 2000 21:38:30 +0100 wenzelm updated;
Thu, 09 Nov 2000 21:38:00 +0100 wenzelm fixed \title: convert "_" to "-";
Wed, 08 Nov 2000 23:04:54 +0100 wenzelm tuned isabelle environment;
Wed, 08 Nov 2000 17:46:24 +0100 nipkow subgoals
Wed, 08 Nov 2000 14:38:04 +0100 nipkow *** empty log message ***
Tue, 07 Nov 2000 18:38:24 +0100 paulson better discussion of rule induction
Tue, 07 Nov 2000 17:55:04 +0100 berghofe Thm.dest_abs now takes an additional argument.
Tue, 07 Nov 2000 17:53:12 +0100 berghofe Moved rewriting functions from Thm to MetaSimplifier.
Tue, 07 Nov 2000 17:52:12 +0100 berghofe - Moved rewriting functions to meta_simplifier.ML
Tue, 07 Nov 2000 17:50:21 +0100 berghofe moved rewriting functions from Drule to MetaSimplifier
Tue, 07 Nov 2000 17:48:25 +0100 berghofe - new theorems imp_cong and swap_prems_eq
Tue, 07 Nov 2000 17:44:48 +0100 berghofe Added new file meta_simplifier.ML
Tue, 07 Nov 2000 17:42:19 +0100 berghofe Moved meta simplification stuff from Thm to MetaSimplifier.
Tue, 07 Nov 2000 17:41:29 +0100 berghofe Added type constraint in theorem "lift".
Tue, 07 Nov 2000 09:33:14 +0100 nipkow *** empty log message ***
Mon, 06 Nov 2000 22:58:26 +0100 wenzelm method 'induct' now handles non-atomic goals;
Mon, 06 Nov 2000 22:56:07 +0100 wenzelm improved: 'induct' handle non-atomic goals;
Mon, 06 Nov 2000 22:54:13 +0100 wenzelm make: open_parms argument;
Mon, 06 Nov 2000 22:53:00 +0100 wenzelm RuleCases.make true;
Mon, 06 Nov 2000 22:52:35 +0100 wenzelm added rewrite_goal_tac;
Mon, 06 Nov 2000 22:50:50 +0100 wenzelm added typ_instance;
Mon, 06 Nov 2000 22:50:01 +0100 wenzelm Sign.typ_instance;
Mon, 06 Nov 2000 22:49:16 +0100 wenzelm inductive_atomize, inductive_rulify;
Mon, 06 Nov 2000 22:48:42 +0100 wenzelm * Isar/HOL: method 'induct' now handles non-atomic goals; as a
Mon, 06 Nov 2000 22:47:41 +0100 wenzelm tuned atomize_goal;
Mon, 06 Nov 2000 18:28:22 +0100 paulson minor modifications for new Springer style
Mon, 06 Nov 2000 16:43:01 +0100 paulson minor changes
Mon, 06 Nov 2000 16:41:39 +0100 paulson auto update
Mon, 06 Nov 2000 11:32:23 +0100 nipkow *** empty log message ***
Sat, 04 Nov 2000 18:54:22 +0100 wenzelm updated;
Sat, 04 Nov 2000 18:44:34 +0100 wenzelm tuned method "rule" and "default";
Sat, 04 Nov 2000 18:42:29 +0100 wenzelm isamarkup: handle % in input;
Sat, 04 Nov 2000 18:41:37 +0100 wenzelm tuned;
Sat, 04 Nov 2000 18:39:44 +0100 wenzelm misc stuff;
Fri, 03 Nov 2000 21:35:59 +0100 wenzelm tuned;
Fri, 03 Nov 2000 21:35:36 +0100 wenzelm proper setup of "parallel";
Fri, 03 Nov 2000 21:34:22 +0100 wenzelm tuned notation;
Fri, 03 Nov 2000 21:33:53 +0100 wenzelm adapted "obtain" proofs;
Fri, 03 Nov 2000 21:33:15 +0100 wenzelm provide case names for rev_induct, rev_cases;
Fri, 03 Nov 2000 21:32:41 +0100 wenzelm rev_exhaust: rulify;
Fri, 03 Nov 2000 21:31:53 +0100 wenzelm removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
Fri, 03 Nov 2000 21:31:11 +0100 wenzelm "atomize" for classical tactics;
Fri, 03 Nov 2000 21:29:56 +0100 wenzelm atomize: all automated tactics that "solve" goals;
Fri, 03 Nov 2000 21:28:15 +0100 wenzelm fixed two obscurities of "fix": predeclare_terms;
Fri, 03 Nov 2000 21:27:36 +0100 wenzelm tuned names;
Fri, 03 Nov 2000 21:27:06 +0100 wenzelm improved handling of "that": insert into goal, only declare as Pure "intro";
Fri, 03 Nov 2000 21:26:11 +0100 wenzelm assumption / finish: handle non-atomic assumptions from context as well;
Fri, 03 Nov 2000 21:25:30 +0100 wenzelm added atomic_judgment;
Fri, 03 Nov 2000 21:25:10 +0100 wenzelm structure Obtain = Obtain;
Fri, 03 Nov 2000 18:33:57 +0100 paulson new lemma card_Diff2_less for mulilated chess board
Fri, 03 Nov 2000 17:57:00 +0100 nipkow *** empty log message ***
Fri, 03 Nov 2000 17:14:06 +0100 nipkow *** empty log message ***
Fri, 03 Nov 2000 16:53:39 +0100 nipkow *** empty log message ***
Fri, 03 Nov 2000 10:26:23 +0100 paulson the section command will belong to the new file
Fri, 03 Nov 2000 10:24:33 +0100 paulson advanced induction examples
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip