Thu, 24 Feb 2000 16:00:28 +0100 wenzelm rN = "record";
Thu, 24 Feb 2000 16:00:09 +0100 wenzelm all_cases / all_inducts;
Thu, 24 Feb 2000 15:59:44 +0100 wenzelm workaround res_inst_tac/lift_inst_rule bug by explicit type contraint;
Thu, 24 Feb 2000 15:58:10 +0100 wenzelm capply, cabs: Sign.nodup_vars;
Thu, 24 Feb 2000 15:57:36 +0100 wenzelm nodup_vars: fixed omission of 2 minor cases; account for Frees as well;
Thu, 24 Feb 2000 15:34:49 +0100 wenzelm tuned generated TeX code;
Thu, 24 Feb 2000 08:56:36 +0100 nipkow renamed a lemma
Thu, 24 Feb 2000 08:55:37 +0100 nipkow Added and renamed a lemma.
Wed, 23 Feb 2000 10:45:08 +0100 paulson not working yet. partial conversion to use "rename" instead of "extend"
Wed, 23 Feb 2000 10:43:02 +0100 paulson new theorems inj_iff, surj_iff
Wed, 23 Feb 2000 10:41:37 +0100 paulson new reference korf85
Tue, 22 Feb 2000 21:53:17 +0100 wenzelm * Pure now provides its own version of intro/elim/dest attributes;
Tue, 22 Feb 2000 21:51:25 +0100 wenzelm tuned syntax wrapper;
Tue, 22 Feb 2000 21:50:02 +0100 wenzelm tuned "induct" syntax;
Tue, 22 Feb 2000 21:49:34 +0100 wenzelm "cases" method;
Tue, 22 Feb 2000 21:48:50 +0100 wenzelm added cases_tac;
Tue, 22 Feb 2000 21:48:24 +0100 wenzelm induct: tuned syntax;
Tue, 22 Feb 2000 21:45:20 +0100 wenzelm added cases_of, cases;
Tue, 22 Feb 2000 21:39:38 +0100 wenzelm removed case_split thm binding;
Tue, 22 Feb 2000 21:39:01 +0100 wenzelm added boolN;
Tue, 22 Feb 2000 20:16:07 +0100 wenzelm proper variant names (admit field "r");
Tue, 22 Feb 2000 10:51:13 +0100 paulson three easy new examples
Mon, 21 Feb 2000 14:10:21 +0100 wenzelm tuned footnote;
Mon, 21 Feb 2000 14:09:40 +0100 wenzelm HOL/record: fixed select-update simplification procedure to handle
Mon, 21 Feb 2000 14:09:18 +0100 wenzelm var: skolem;
Mon, 21 Feb 2000 14:08:15 +0100 wenzelm remove *.out;
Mon, 21 Feb 2000 13:57:07 +0100 oheimb renamed Univalent to univalent
Mon, 21 Feb 2000 11:16:19 +0100 paulson simplified some proofs
Mon, 21 Feb 2000 11:15:43 +0100 paulson new examples that cannot be done in LEO
Mon, 21 Feb 2000 10:20:38 +0100 nipkow A few lemmas and some Adds.
Sun, 20 Feb 2000 09:32:06 +0100 nipkow Added global let-simplification rule.
Sat, 19 Feb 2000 13:47:12 +0100 nipkow Commenst.
Fri, 18 Feb 2000 20:27:19 +0100 oheimb added instance declaration for finite product
Fri, 18 Feb 2000 20:25:29 +0100 oheimb added split_eta_SetCompr, SetCompr_Sigma_eq
Fri, 18 Feb 2000 20:24:56 +0100 oheimb added Suc_le_D
Fri, 18 Feb 2000 20:24:40 +0100 oheimb added domI, domD
Fri, 18 Feb 2000 20:24:16 +0100 oheimb changed precedence of function update
Fri, 18 Feb 2000 18:29:28 +0100 nipkow installed lin arith for nat numerals.
Fri, 18 Feb 2000 15:37:08 +0100 paulson Rename: theory for applying a bijection over states to a UNITY program
Fri, 18 Feb 2000 15:35:29 +0100 paulson new distributive laws
Fri, 18 Feb 2000 15:34:22 +0100 paulson expandshort
Fri, 18 Feb 2000 15:33:09 +0100 paulson many new theorems about inj, surj etc.
Fri, 18 Feb 2000 15:28:32 +0100 paulson new theorem nat_diff_split'
Fri, 18 Feb 2000 15:20:44 +0100 paulson New treatment of "guarantees" with polymorphic components and bijections.
Wed, 16 Feb 2000 15:04:12 +0100 wenzelm Syntax translation functions;
Wed, 16 Feb 2000 10:51:23 +0100 paulson fixed some overfull lines
Wed, 16 Feb 2000 10:50:57 +0100 paulson a smaller point size reduces the number of overfull figures
Tue, 15 Feb 2000 21:02:55 +0100 kleing cosmetics
Tue, 15 Feb 2000 19:41:44 +0100 wenzelm fixed sel_upd simproc (less efficient, but more complete);
Tue, 15 Feb 2000 17:51:11 +0100 kleing lightweight bytecode verifier with correctness proof
Mon, 14 Feb 2000 20:49:08 +0100 wenzelm basic source deps;
Mon, 14 Feb 2000 20:43:12 +0100 wenzelm easy_setup: fixed mksimps;
Mon, 14 Feb 2000 20:42:02 +0100 wenzelm proof step: reset goal_facts;
Mon, 14 Feb 2000 12:23:08 +0100 wenzelm mkdir -p $ISABELLE_BROWSER_INFO;
Mon, 14 Feb 2000 11:23:57 +0100 wenzelm fixed prefer;
Mon, 14 Feb 2000 11:23:44 +0100 wenzelm tuned msg;
Sun, 13 Feb 2000 21:01:26 +0100 wenzelm added refine_end;
Sun, 13 Feb 2000 21:00:02 +0100 wenzelm tuned attrib;
Sun, 13 Feb 2000 20:58:13 +0100 wenzelm apply: observe facts;
Sun, 13 Feb 2000 20:56:55 +0100 wenzelm prf_script commands made proper;
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip