Sun, 26 Mar 2000 20:16:34 +0200 wenzelm tuned;
Sun, 26 Mar 2000 20:13:53 +0200 wenzelm ignore_stuff;
Sun, 26 Mar 2000 20:12:28 +0200 wenzelm tuned output;
Sun, 26 Mar 2000 20:11:12 +0200 wenzelm !!!! = cut "Corrupted outer syntax in presentation";
Sun, 26 Mar 2000 20:10:31 +0200 wenzelm added is_begin/end_ignore;
Sun, 26 Mar 2000 20:08:03 +0200 wenzelm tuned targets;
Sat, 25 Mar 2000 18:01:27 +0100 wenzelm tuned;
Sat, 25 Mar 2000 17:59:52 +0100 wenzelm improved (anti)quote_tr(');
Sat, 25 Mar 2000 13:00:44 +0100 wenzelm addsimprocs [record_simproc];
Sat, 25 Mar 2000 12:59:31 +0100 wenzelm tuned antiquote_tr';
Sat, 25 Mar 2000 12:52:06 +0100 wenzelm export updateN;
Fri, 24 Mar 2000 21:15:56 +0100 wenzelm use abstract syntax;
Fri, 24 Mar 2000 21:09:34 +0100 wenzelm plain ASCII;
Fri, 24 Mar 2000 20:59:15 +0100 wenzelm arith method: HEADGOAL;
Fri, 24 Mar 2000 17:29:51 +0100 wenzelm HOL/ex/Multiquote;
Fri, 24 Mar 2000 17:28:03 +0100 wenzelm added HOL/ex/Multiquote.thy;
Fri, 24 Mar 2000 14:40:51 +0100 wenzelm tuned;
Fri, 24 Mar 2000 13:48:31 +0100 wenzelm usedir -D: update styles as well;
Fri, 24 Mar 2000 13:48:01 +0100 wenzelm usedir -D: update styles;
Fri, 24 Mar 2000 13:47:36 +0100 wenzelm improved dump of styles;
Fri, 24 Mar 2000 11:52:19 +0100 wenzelm -o sty;
Fri, 24 Mar 2000 08:56:48 +0100 nipkow comments
Thu, 23 Mar 2000 21:37:13 +0100 wenzelm added 'moreover' command;
Thu, 23 Mar 2000 21:36:43 +0100 wenzelm tuned output;
Thu, 23 Mar 2000 11:28:10 +0100 wenzelm tuned spacing;
Thu, 23 Mar 2000 11:27:52 +0100 wenzelm ex/Antiquote.thy made new-style theory;
Thu, 23 Mar 2000 10:23:54 +0100 paulson now exclusively uses rtac/dtac/etac rather than the long forms
Thu, 23 Mar 2000 10:22:08 +0100 paulson restored the MESON examples file HOL/ex/mesontest2.ML
Wed, 22 Mar 2000 13:23:57 +0100 paulson made a proof more robust (did not like Suc_less_eq)
Wed, 22 Mar 2000 13:22:39 +0100 paulson Suc_less_eq now with AddIffs. How could this have been overlooked?
Wed, 22 Mar 2000 13:22:11 +0100 paulson combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
Wed, 22 Mar 2000 13:01:57 +0100 paulson made more robust
Wed, 22 Mar 2000 13:01:18 +0100 paulson tidied using new "inst" rule
Wed, 22 Mar 2000 12:45:41 +0100 paulson tidied using new "inst" rule
Wed, 22 Mar 2000 12:33:34 +0100 paulson new meta-rule "inst", a shorthand for read_instantiate_sg
Tue, 21 Mar 2000 17:43:54 +0100 wenzelm goal_spec: [!];
Tue, 21 Mar 2000 17:32:44 +0100 wenzelm tuned;
Tue, 21 Mar 2000 17:32:43 +0100 wenzelm tuned;
Tue, 21 Mar 2000 15:32:08 +0100 wenzelm tuned;
Tue, 21 Mar 2000 15:26:21 +0100 wenzelm tuned comment;
Tue, 21 Mar 2000 15:23:33 +0100 wenzelm help message;
Tue, 21 Mar 2000 00:18:54 +0100 wenzelm handle general case: params and hyps of thesis;
Tue, 21 Mar 2000 00:17:56 +0100 wenzelm soft_asm_tac: hack to norm goal;
Mon, 20 Mar 2000 18:49:14 +0100 wenzelm proof methods: 'case_tac' / 'induct_tac';
Mon, 20 Mar 2000 18:48:43 +0100 wenzelm tuned degenerate cases / induct;
Mon, 20 Mar 2000 18:48:12 +0100 wenzelm added prove_goalw_cterm;
Mon, 20 Mar 2000 18:47:47 +0100 wenzelm quick_and_dirty moved to Isar/skip_proof.ML;
Mon, 20 Mar 2000 18:47:27 +0100 wenzelm use Args.goal_spec;
Mon, 20 Mar 2000 18:47:07 +0100 wenzelm goal_spec;
Mon, 20 Mar 2000 18:46:53 +0100 wenzelm ALLGOALS_RANGE superceded by Seq.INTERVAL;
Mon, 20 Mar 2000 18:45:28 +0100 wenzelm improved support for emulating tactic scripts;
Mon, 20 Mar 2000 18:43:37 +0100 wenzelm res_inst_tac etc.;
Mon, 20 Mar 2000 18:43:20 +0100 wenzelm goalspec;
Mon, 20 Mar 2000 18:43:05 +0100 wenzelm case_tac, induct_tac;
Mon, 20 Mar 2000 18:42:50 +0100 wenzelm tactic emulation;
Mon, 20 Mar 2000 18:25:35 +0100 paulson tidied
Mon, 20 Mar 2000 18:24:11 +0100 paulson the perm_rules variable is no longer needed
Mon, 20 Mar 2000 12:54:31 +0100 paulson tidied
Mon, 20 Mar 2000 11:15:28 +0100 paulson replaced best_tac by force_tac, allowing some arithmetic reasoning
Mon, 20 Mar 2000 10:32:02 +0100 paulson renamed a variable to avoid possible free/bound confusion
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip