| Mon, 06 Nov 2000 22:52:35 +0100 | wenzelm | added rewrite_goal_tac; | changeset | files |
| Mon, 06 Nov 2000 22:50:50 +0100 | wenzelm | added typ_instance; | changeset | files |
| Mon, 06 Nov 2000 22:50:01 +0100 | wenzelm | Sign.typ_instance; | changeset | files |
| Mon, 06 Nov 2000 22:49:16 +0100 | wenzelm | inductive_atomize, inductive_rulify; | changeset | files |
| Mon, 06 Nov 2000 22:48:42 +0100 | wenzelm | * Isar/HOL: method 'induct' now handles non-atomic goals; as a | changeset | files |
| Mon, 06 Nov 2000 22:47:41 +0100 | wenzelm | tuned atomize_goal; | changeset | files |
| Mon, 06 Nov 2000 18:28:22 +0100 | paulson | minor modifications for new Springer style | changeset | files |
| Mon, 06 Nov 2000 16:43:01 +0100 | paulson | minor changes | changeset | files |
| Mon, 06 Nov 2000 16:41:39 +0100 | paulson | auto update | changeset | files |
| Mon, 06 Nov 2000 11:32:23 +0100 | nipkow | *** empty log message *** | changeset | files |
| Sat, 04 Nov 2000 18:54:22 +0100 | wenzelm | updated; | changeset | files |
| Sat, 04 Nov 2000 18:44:34 +0100 | wenzelm | tuned method "rule" and "default"; | changeset | files |
| Sat, 04 Nov 2000 18:42:29 +0100 | wenzelm | isamarkup: handle % in input; | changeset | files |
| Sat, 04 Nov 2000 18:41:37 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 04 Nov 2000 18:39:44 +0100 | wenzelm | misc stuff; | changeset | files |
| Fri, 03 Nov 2000 21:35:59 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 03 Nov 2000 21:35:36 +0100 | wenzelm | proper setup of "parallel"; | changeset | files |
| Fri, 03 Nov 2000 21:34:22 +0100 | wenzelm | tuned notation; | changeset | files |
| Fri, 03 Nov 2000 21:33:53 +0100 | wenzelm | adapted "obtain" proofs; | changeset | files |
| Fri, 03 Nov 2000 21:33:15 +0100 | wenzelm | provide case names for rev_induct, rev_cases; | changeset | files |
| Fri, 03 Nov 2000 21:32:41 +0100 | wenzelm | rev_exhaust: rulify; | changeset | files |
| Fri, 03 Nov 2000 21:31:53 +0100 | wenzelm | removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML); | changeset | files |
| Fri, 03 Nov 2000 21:31:11 +0100 | wenzelm | "atomize" for classical tactics; | changeset | files |
| Fri, 03 Nov 2000 21:29:56 +0100 | wenzelm | atomize: all automated tactics that "solve" goals; | changeset | files |
| Fri, 03 Nov 2000 21:28:15 +0100 | wenzelm | fixed two obscurities of "fix": predeclare_terms; | changeset | files |
| Fri, 03 Nov 2000 21:27:36 +0100 | wenzelm | tuned names; | changeset | files |
| Fri, 03 Nov 2000 21:27:06 +0100 | wenzelm | improved handling of "that": insert into goal, only declare as Pure "intro"; | changeset | files |
| Fri, 03 Nov 2000 21:26:11 +0100 | wenzelm | assumption / finish: handle non-atomic assumptions from context as well; | changeset | files |
| Fri, 03 Nov 2000 21:25:30 +0100 | wenzelm | added atomic_judgment; | changeset | files |
| Fri, 03 Nov 2000 21:25:10 +0100 | wenzelm | structure Obtain = Obtain; | changeset | files |
| Fri, 03 Nov 2000 18:33:57 +0100 | paulson | new lemma card_Diff2_less for mulilated chess board | changeset | files |
| Fri, 03 Nov 2000 17:57:00 +0100 | nipkow | *** empty log message *** | changeset | files |
| Fri, 03 Nov 2000 17:14:06 +0100 | nipkow | *** empty log message *** | changeset | files |
| Fri, 03 Nov 2000 16:53:39 +0100 | nipkow | *** empty log message *** | changeset | files |
| Fri, 03 Nov 2000 10:26:23 +0100 | paulson | the section command will belong to the new file | changeset | files |
| Fri, 03 Nov 2000 10:24:33 +0100 | paulson | advanced induction examples | changeset | files |
| Fri, 03 Nov 2000 10:24:06 +0100 | paulson | auto update? | changeset | files |
| Fri, 03 Nov 2000 10:23:24 +0100 | paulson | replaced Acc.thy by Advanced.thy | changeset | files |
| Thu, 02 Nov 2000 15:45:32 +0100 | paulson | no longer needed: too complicated an example | changeset | files |
| Thu, 02 Nov 2000 15:44:13 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 02 Nov 2000 11:00:29 +0100 | paulson | auto generated | changeset | files |
| Tue, 31 Oct 2000 20:33:10 +0100 | wenzelm | tuned goal output; | changeset | files |
| Tue, 31 Oct 2000 13:59:41 +0100 | nipkow | *** empty log message *** | changeset | files |
| Tue, 31 Oct 2000 08:53:12 +0100 | nipkow | *** empty log message *** | changeset | files |
| Mon, 30 Oct 2000 18:28:00 +0100 | wenzelm | updated; | changeset | files |
| Mon, 30 Oct 2000 18:26:14 +0100 | wenzelm | tuned goals output; | changeset | files |
| Mon, 30 Oct 2000 18:25:38 +0100 | wenzelm | improved statement bindings for props; | changeset | files |
| Mon, 30 Oct 2000 18:25:10 +0100 | wenzelm | converse: syntax \<inverse>; | changeset | files |
| Mon, 30 Oct 2000 18:24:42 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 30 Oct 2000 18:24:20 +0100 | wenzelm | added ex/PER.thy; | changeset | files |
| Mon, 30 Oct 2000 18:23:34 +0100 | wenzelm | improved doc of "subgoals" antiquotation; | changeset | files |
| Mon, 30 Oct 2000 18:22:49 +0100 | wenzelm | replaced \isasymmacron by \isasyminverse; | changeset | files |
| Mon, 30 Oct 2000 18:22:20 +0100 | wenzelm | tuned tex template; | changeset | files |
| Mon, 30 Oct 2000 18:21:45 +0100 | wenzelm | Partial equivalence relations (leftover from HOL/Quot); | changeset | files |
| Mon, 30 Oct 2000 08:40:05 +0100 | nipkow | added antiq. subgoals | changeset | files |
| Mon, 30 Oct 2000 08:34:37 +0100 | nipkow | Added antiquotation "subgoals". | changeset | files |
| Mon, 30 Oct 2000 08:34:12 +0100 | nipkow | Mod because of additional parameters to pretty_goals. | changeset | files |
| Fri, 27 Oct 2000 16:25:21 +0200 | wenzelm | back to 1.167, due to Emacs/CVS casualty!!; | changeset | files |
| Fri, 27 Oct 2000 15:53:47 +0200 | oheimb | added instantiate_tac | changeset | files |
| Fri, 27 Oct 2000 15:23:39 +0200 | wenzelm | *** empty log message *** | changeset | files |