Sun, 16 Jul 2000 20:46:44 +0200 wenzelm * tuned AST representation of nested pairs, avoiding bogus output in
Fri, 14 Jul 2000 20:47:11 +0200 oheimb corrections (cast relation, Prog.ML -> Decl.ML)
Fri, 14 Jul 2000 17:49:56 +0200 wenzelm improved add_edges_cyclic;
Fri, 14 Jul 2000 16:32:51 +0200 oheimb re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
Fri, 14 Jul 2000 16:32:44 +0200 oheimb added (surjective_pairing RS sym) to simpset
Fri, 14 Jul 2000 16:29:02 +0200 oheimb strengthened rtranclD
Fri, 14 Jul 2000 16:28:58 +0200 oheimb added option_map_o_sum_case (also to simpset)
Fri, 14 Jul 2000 16:28:56 +0200 oheimb added sum_case_empty_empty (also to simpset)
Fri, 14 Jul 2000 16:28:49 +0200 oheimb tuned syntax
Fri, 14 Jul 2000 16:27:45 +0200 oheimb added hint on fun_sum
Fri, 14 Jul 2000 16:27:42 +0200 oheimb added fun_upd2_simproc
Fri, 14 Jul 2000 16:27:37 +0200 oheimb re-added subset_empty to simpset
Fri, 14 Jul 2000 14:51:02 +0200 paulson used bounded quantification in definition of guarantees and other minor
Fri, 14 Jul 2000 14:47:15 +0200 paulson moved sublist from UNITY/AllocBase to List
Fri, 14 Jul 2000 14:46:35 +0200 paulson AddIffs
Fri, 14 Jul 2000 13:57:00 +0200 paulson parent should be Main
Fri, 14 Jul 2000 13:39:03 +0200 paulson changed the quotient syntax from / to //
Thu, 13 Jul 2000 23:26:08 +0200 wenzelm tuned cycle_msg;
Thu, 13 Jul 2000 23:23:24 +0200 wenzelm updated;
Thu, 13 Jul 2000 23:22:26 +0200 wenzelm HOL: the disjoint sum is now "<+>" instead of "Plus";
Thu, 13 Jul 2000 23:20:57 +0200 wenzelm adapted PureThy.add_defs_i;
Thu, 13 Jul 2000 23:20:33 +0200 wenzelm defs (overloaded);
Thu, 13 Jul 2000 23:20:14 +0200 wenzelm tuned;
Thu, 13 Jul 2000 23:19:40 +0200 wenzelm added read_xnum;
Thu, 13 Jul 2000 23:19:08 +0200 wenzelm fix(_i): admit internal variables;
Thu, 13 Jul 2000 23:18:36 +0200 wenzelm use ProofContext.bind_skolem;
Thu, 13 Jul 2000 23:17:44 +0200 wenzelm defs: (overloaded) option;
Thu, 13 Jul 2000 23:17:14 +0200 wenzelm eq_prop: strip_assums_concl;
Thu, 13 Jul 2000 23:16:48 +0200 wenzelm tuned exceptions;
Thu, 13 Jul 2000 23:16:13 +0200 wenzelm const_deps: unit Graph.T;
Thu, 13 Jul 2000 23:15:20 +0200 wenzelm add_term_consts: ins_string;
Thu, 13 Jul 2000 23:14:49 +0200 wenzelm add_defs(_i): overloaded option;
Thu, 13 Jul 2000 23:14:15 +0200 wenzelm adapted PureThy.add_defs;
Thu, 13 Jul 2000 23:13:52 +0200 wenzelm fixed comment;
Thu, 13 Jul 2000 23:13:10 +0200 wenzelm adapted PureThy.add_defs_i;
Thu, 13 Jul 2000 23:11:38 +0200 wenzelm use Syntax.read_xnum;
Thu, 13 Jul 2000 23:11:14 +0200 wenzelm fixed simplified_cases;
Thu, 13 Jul 2000 23:10:12 +0200 wenzelm fixed name: UN_empty3;
Thu, 13 Jul 2000 23:09:25 +0200 wenzelm replaced infix Plus by <+>;
Thu, 13 Jul 2000 23:09:03 +0200 wenzelm removed duplicate Compl_atMost;
Thu, 13 Jul 2000 23:08:42 +0200 wenzelm fixed compose decl;
Thu, 13 Jul 2000 23:08:20 +0200 wenzelm defs: (overloaded) option;
Thu, 13 Jul 2000 23:07:56 +0200 wenzelm method cases/induct: (opaque) option;
Thu, 13 Jul 2000 23:07:10 +0200 wenzelm defs (overloaded);
Thu, 13 Jul 2000 13:05:58 +0200 paulson removed now-redundant proof steps
Thu, 13 Jul 2000 13:04:48 +0200 paulson added an important default rule
Thu, 13 Jul 2000 13:02:20 +0200 paulson fixed a failing proof
Thu, 13 Jul 2000 13:00:22 +0200 paulson le_refl_iff as default rule
Thu, 13 Jul 2000 12:59:26 +0200 paulson removed needless premises
Thu, 13 Jul 2000 12:56:42 +0200 paulson AddIffs now available for FOL, ZF
Thu, 13 Jul 2000 11:44:02 +0200 wenzelm added simp_case_tac;
Thu, 13 Jul 2000 11:42:11 +0200 wenzelm use InductMethod.simp_case_tac;
Thu, 13 Jul 2000 11:41:40 +0200 wenzelm tuned;
Thu, 13 Jul 2000 11:41:06 +0200 wenzelm export thesisN separately;
Thu, 13 Jul 2000 11:40:49 +0200 wenzelm prep rhs in original context;
Thu, 13 Jul 2000 11:39:41 +0200 wenzelm RuleCases.make opaq;
Thu, 13 Jul 2000 11:39:22 +0200 wenzelm bind_skolem;
Thu, 13 Jul 2000 11:39:03 +0200 wenzelm invoke_case: bind_skolem;
Thu, 13 Jul 2000 11:38:42 +0200 wenzelm "_i" arguments now expected to have skolems already internalized;
Thu, 13 Jul 2000 11:36:57 +0200 wenzelm make: opaq flag;
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip