Sat, 19 Aug 2000 12:43:55 +0200 wenzelm added \isachar definitions;
Sat, 19 Aug 2000 12:42:52 +0200 wenzelm %\urlstyle{rm}
Sat, 19 Aug 2000 12:41:41 +0200 wenzelm renamed cond_with_path to cond_add_path (add to front);
Fri, 18 Aug 2000 18:46:02 +0200 paulson X-symbols for ordinal, cardinal, integer arithmetic
Fri, 18 Aug 2000 18:11:10 +0200 wenzelm fixed RuleCases.make (invert flag);
Fri, 18 Aug 2000 18:06:10 +0200 wenzelm removed obsolete add_recdef_x;
Fri, 18 Aug 2000 17:58:33 +0200 wenzelm proper handling of defs;
Fri, 18 Aug 2000 17:53:49 +0200 wenzelm Main now new-style theory; added Main.ML for compatibility;
Fri, 18 Aug 2000 12:34:48 +0200 paulson simproc bug fix: only TYPING assumptions are given to the simplifier
Fri, 18 Aug 2000 12:34:13 +0200 paulson better rules for cancellation of common factors across comparisons
Fri, 18 Aug 2000 12:31:20 +0200 paulson new example ZF/ex/NatSum
Fri, 18 Aug 2000 12:30:41 +0200 paulson now allows dest_coeff to fail
Fri, 18 Aug 2000 11:14:23 +0200 nipkow *** empty log message ***
Fri, 18 Aug 2000 10:34:08 +0200 nipkow *** empty log message ***
Thu, 17 Aug 2000 21:07:25 +0200 wenzelm removed obsolete keyword;
Thu, 17 Aug 2000 21:06:04 +0200 wenzelm fixed indexing;
Thu, 17 Aug 2000 18:58:49 +0200 wenzelm tuned;
Thu, 17 Aug 2000 18:31:12 +0200 nipkow installed recdef congs data
Thu, 17 Aug 2000 18:30:48 +0200 nipkow added map_cong to recdef
Thu, 17 Aug 2000 16:23:50 +0200 wenzelm removed Lambda/Type.ML;
Thu, 17 Aug 2000 12:02:01 +0200 paulson better rules for cancellation of common factors across comparisons
Thu, 17 Aug 2000 12:01:09 +0200 paulson fixed a proof that had stopped working ???
Thu, 17 Aug 2000 12:00:23 +0200 paulson tidied & updated proofs, deleting some unused ones
Thu, 17 Aug 2000 11:56:47 +0200 paulson modified proofs: better rules for cancellation of common factors across comparisons
Thu, 17 Aug 2000 11:55:47 +0200 paulson better rules for cancellation of common factors across comparisons
Thu, 17 Aug 2000 10:42:57 +0200 wenzelm *** empty log message ***
Thu, 17 Aug 2000 10:40:31 +0200 wenzelm cases: opaque by default;
Thu, 17 Aug 2000 10:39:44 +0200 wenzelm renamed 'RS' to 'THEN';
Thu, 17 Aug 2000 10:39:30 +0200 wenzelm tuned error handling;
Thu, 17 Aug 2000 10:39:12 +0200 wenzelm added 'symmetric' attribute;
Thu, 17 Aug 2000 10:38:43 +0200 wenzelm updated;
Thu, 17 Aug 2000 10:38:20 +0200 wenzelm sel_upd proc: include 'more' pseudo-field;
Thu, 17 Aug 2000 10:37:33 +0200 wenzelm renamed 'mk_cases_tac' to 'ind_cases';
Thu, 17 Aug 2000 10:37:04 +0200 wenzelm changed 'opaque' option to 'open' (opaque is default);
Thu, 17 Aug 2000 10:35:49 +0200 wenzelm renamed 'RS' to 'THEN';
Thu, 17 Aug 2000 10:34:52 +0200 wenzelm converted to new-style theory;
Thu, 17 Aug 2000 10:34:28 +0200 wenzelm done;
Thu, 17 Aug 2000 10:34:11 +0200 wenzelm 'symmetric' attribute;
Thu, 17 Aug 2000 10:33:37 +0200 wenzelm fixed deps;
Thu, 17 Aug 2000 10:33:13 +0200 wenzelm renamed 'RS' to 'THEN';
Thu, 17 Aug 2000 10:32:44 +0200 wenzelm index tokens;
Thu, 17 Aug 2000 10:32:20 +0200 wenzelm cases/induct method: 'opaque' by default; added 'open' option;
Thu, 17 Aug 2000 10:31:43 +0200 wenzelm updated;
Thu, 17 Aug 2000 10:31:10 +0200 wenzelm renamed 'RS' to 'THEN';
Thu, 17 Aug 2000 10:29:50 +0200 wenzelm fixed lbrace, rbrace;
Thu, 17 Aug 2000 10:29:23 +0200 wenzelm Isar/Pure: renamed 'RS' attribute to 'THEN';
Wed, 16 Aug 2000 18:10:15 +0200 nipkow Fixed completeness bug in simplifier: congruence rules could preclude
Wed, 16 Aug 2000 10:25:02 +0200 paulson major sharpening of stable_project_transient
Wed, 16 Aug 2000 10:23:25 +0200 paulson new (unused) lemma
Wed, 16 Aug 2000 10:22:41 +0200 paulson new thm and simprule Compl_Diff_eq
Mon, 14 Aug 2000 18:49:35 +0200 wenzelm added conversion.tex;
Mon, 14 Aug 2000 18:49:23 +0200 wenzelm moved tactic emulation methods here;
Mon, 14 Aug 2000 18:47:32 +0200 wenzelm added 'declare' command;
Mon, 14 Aug 2000 18:45:49 +0200 wenzelm tuned;
Mon, 14 Aug 2000 18:45:31 +0200 wenzelm updated;
Mon, 14 Aug 2000 18:45:16 +0200 wenzelm renamed 'intrs' to 'intros';
Mon, 14 Aug 2000 18:43:57 +0200 wenzelm updated command termination issue;
Mon, 14 Aug 2000 18:43:30 +0200 wenzelm some more refs;
Mon, 14 Aug 2000 18:42:57 +0200 wenzelm Aspinall:2000:eProof;
Mon, 14 Aug 2000 18:14:54 +0200 wenzelm raplaced "intrs" by "intrs" (new-style only);
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip