Sun, 30 Jan 2000 13:24:41 +0100 wenzelm rm -f *.aux;
Sat, 29 Jan 2000 14:22:16 +0100 wenzelm simp_all method;
Fri, 28 Jan 2000 21:58:39 +0100 wenzelm eliminated proof script;
Fri, 28 Jan 2000 21:57:15 +0100 wenzelm HEADGOAL;
Fri, 28 Jan 2000 21:56:55 +0100 wenzelm added prefer, defer;
Fri, 28 Jan 2000 21:56:37 +0100 wenzelm added HEADGOAL;
Fri, 28 Jan 2000 21:56:02 +0100 wenzelm added defer, prefer;
Fri, 28 Jan 2000 21:55:43 +0100 wenzelm Drule.instantiate;
Fri, 28 Jan 2000 21:55:23 +0100 wenzelm cp -r;
Fri, 28 Jan 2000 15:26:51 +0100 wenzelm -p option;
Fri, 28 Jan 2000 15:08:15 +0100 oheimb added range_composition (also to simpset)
Fri, 28 Jan 2000 14:49:00 +0100 oheimb added finite_range_updI, finite_range_map_of, finite_range_map_of_override
Fri, 28 Jan 2000 14:42:46 +0100 wenzelm mkdir: prepare logic session directory;
Fri, 28 Jan 2000 14:09:23 +0100 oheimb added full_nat_induct
Fri, 28 Jan 2000 14:08:54 +0100 oheimb added splitE', also to claset
Fri, 28 Jan 2000 14:07:53 +0100 oheimb added inj_singleton
Fri, 28 Jan 2000 14:07:33 +0100 oheimb added finite_range_imageI
Fri, 28 Jan 2000 12:12:06 +0100 wenzelm replaced FIRSTGOAL by FINDGOAL (backtracking!);
Fri, 28 Jan 2000 12:10:47 +0100 wenzelm maintain standard rules (beware: classical provers provides another version!);
Fri, 28 Jan 2000 12:06:52 +0100 wenzelm replaced FIRSTGOAL by FINDGOAL (backtracking!);
Fri, 28 Jan 2000 12:04:17 +0100 wenzelm tuned sig;
Fri, 28 Jan 2000 12:03:59 +0100 wenzelm map data;
Fri, 28 Jan 2000 11:23:41 +0100 oheimb added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
Fri, 28 Jan 2000 11:22:02 +0100 oheimb beautified spacing for binders with symbols syntax, analogous to HOL.thy
Thu, 27 Jan 2000 15:30:10 +0100 oheimb *** empty log message ***
Wed, 26 Jan 2000 21:12:40 +0100 wenzelm 'name' etc. include 'number';
Wed, 26 Jan 2000 21:10:27 +0100 wenzelm 'name' syntax includes numbers;
Wed, 26 Jan 2000 11:04:38 +0100 nipkow optimized xs[i:=x]!j lemmas.
Tue, 25 Jan 2000 22:31:53 +0100 wenzelm added map, map_st;
Tue, 25 Jan 2000 22:28:48 +0100 wenzelm added map;
Tue, 25 Jan 2000 20:22:57 +0100 wenzelm fallback on PureThy version;
Tue, 25 Jan 2000 09:25:43 +0100 nipkow replaced f : A funcset B by f``A <= B.
Mon, 24 Jan 2000 14:48:11 +0100 kleing reflexivity simp rules
Fri, 21 Jan 2000 10:45:40 +0100 paulson new theorem inj_on_restrict_eq
Thu, 20 Jan 2000 17:57:59 +0100 wenzelm removed Isar_examples/Minimal;
Tue, 18 Jan 2000 11:33:31 +0100 paulson fixed many bad line & page breaks
Tue, 18 Jan 2000 11:00:10 +0100 paulson Documented Thm.instantiate (not normalizing) and Drule.instantiate
Mon, 17 Jan 2000 15:56:58 +0100 wenzelm www;
Mon, 17 Jan 2000 15:51:37 +0100 kleing Id line inserted
Mon, 17 Jan 2000 15:49:55 +0100 kleing changes for the makepage script in Admin
Mon, 17 Jan 2000 15:49:32 +0100 kleing makes Isabelle main web pages
Mon, 17 Jan 2000 15:02:18 +0100 wenzelm Contents: suppress comments;
Mon, 17 Jan 2000 14:10:32 +0100 paulson Thm.instantiate no longer normalizes, but Drule.instantiate does
Fri, 14 Jan 2000 12:17:53 +0100 paulson still working; a bit of polishing
Thu, 13 Jan 2000 17:36:58 +0100 paulson new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
Thu, 13 Jan 2000 17:36:02 +0100 paulson change for new rewriting
Thu, 13 Jan 2000 17:34:59 +0100 paulson added recursor
Thu, 13 Jan 2000 17:34:39 +0100 paulson change in add_thmss to suppress warning
Thu, 13 Jan 2000 17:31:30 +0100 paulson a bit of tidying
Thu, 13 Jan 2000 17:30:23 +0100 paulson working version, with Alloc now working on the same state space as the whole
Thu, 13 Jan 2000 17:29:04 +0100 paulson new theorem subset_Compl_self_eq
Thu, 13 Jan 2000 15:29:52 +0100 wenzelm tuned comment;
Wed, 12 Jan 2000 15:58:16 +0100 nipkow Move some lemmas to List.
Wed, 12 Jan 2000 15:58:01 +0100 nipkow More lemmas.
Mon, 10 Jan 2000 17:08:41 +0100 wenzelm isabellesimple: avoid paragraph;
Mon, 10 Jan 2000 16:07:29 +0100 nipkow int:nat->int is pushed inwards.
Mon, 10 Jan 2000 16:06:43 +0100 nipkow Forgot to "call" MicroJava in makefile.
Fri, 07 Jan 2000 11:06:03 +0100 paulson tidied parentheses
Fri, 07 Jan 2000 11:04:15 +0100 paulson tidied
Fri, 07 Jan 2000 11:00:56 +0100 paulson new theorem leadsTo_refl and induction rule leadsTo_induct_pre
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip