huffman [Sat, 25 Jun 2005 01:04:01 +0200] rev 16564
cleaned up proof of contlub_abstraction
paulson [Fri, 24 Jun 2005 17:25:10 +0200] rev 16563
meson method taking an argument list
paulson [Fri, 24 Jun 2005 16:21:01 +0200] rev 16562
deleted a redundant "use" line
paulson [Fri, 24 Jun 2005 16:18:41 +0200] rev 16561
tidying
paulson [Fri, 24 Jun 2005 13:22:08 +0200] rev 16560
stylistic tweaks concerning Find
kleing [Fri, 24 Jun 2005 04:18:48 +0200] rev 16559
shortened time out by 3h (gives up at 12:00h now).
test should be finished by 10:00h usually.
kleing [Fri, 24 Jun 2005 03:16:52 +0200] rev 16558
made su[bp]/isu[bp] behave the same as their bsu[bp]..esu[bp] counterparts,
properly respect isastylescript now
kleing [Fri, 24 Jun 2005 01:09:16 +0200] rev 16557
needed for Isabelle independent build
huffman [Thu, 23 Jun 2005 22:11:55 +0200] rev 16556
added theorems fix_strict, fix_defined, fix_id, fix_const
huffman [Thu, 23 Jun 2005 22:10:29 +0200] rev 16555
add binder syntax for flift1
huffman [Thu, 23 Jun 2005 22:08:24 +0200] rev 16554
add new file to test fixrec package
huffman [Thu, 23 Jun 2005 22:07:30 +0200] rev 16553
add csplit3, ssplit3, fup3 as simp rules
huffman [Thu, 23 Jun 2005 21:27:23 +0200] rev 16552
New features:
permissive option for fixrec to skip proofs of equations;
side conditions for fixrec equations (for definedness);
fixpat theorem names apply to entire group of theorems;
improved error messages
huffman [Thu, 23 Jun 2005 21:17:26 +0200] rev 16551
added match functions for spair, sinl, sinr
nipkow [Thu, 23 Jun 2005 19:40:03 +0200] rev 16550
fixed \<Prod> syntax
nipkow [Thu, 23 Jun 2005 07:32:59 +0200] rev 16549
new
quigley [Wed, 22 Jun 2005 20:26:31 +0200] rev 16548
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
Will now signal if ATP has run out of time and then kill the watcher.
wenzelm [Wed, 22 Jun 2005 19:48:20 +0200] rev 16547
* Pure: the Isar proof context type is already defined early in Pure
as Context.proof;
nipkow [Wed, 22 Jun 2005 19:44:12 +0200] rev 16546
added find2
nipkow [Wed, 22 Jun 2005 19:44:03 +0200] rev 16545
*** empty log message ***
nipkow [Wed, 22 Jun 2005 19:43:48 +0200] rev 16544
tunes Find
nipkow [Wed, 22 Jun 2005 19:43:38 +0200] rev 16543
added Rules/find2
wenzelm [Wed, 22 Jun 2005 19:41:30 +0200] rev 16542
tuned pointer_eq;
wenzelm [Wed, 22 Jun 2005 19:41:29 +0200] rev 16541
renamed data kind;
wenzelm [Wed, 22 Jun 2005 19:41:28 +0200] rev 16540
removed proof data (see Pure/context.ML);
wenzelm [Wed, 22 Jun 2005 19:41:27 +0200] rev 16539
added depth_of;
wenzelm [Wed, 22 Jun 2005 19:41:24 +0200] rev 16538
removed obsolete object.ML (see Pure/library.ML);
wenzelm [Wed, 22 Jun 2005 19:41:23 +0200] rev 16537
export sort_ord;
tuned term_ord, typ_ord: use pointer_eq;
tuned aconv, aconvs: based on term_ord;
wenzelm [Wed, 22 Jun 2005 19:41:22 +0200] rev 16536
renamed init to init_data;
wenzelm [Wed, 22 Jun 2005 19:41:20 +0200] rev 16535
added structure Object (from Pure/General/object.ML);
wenzelm [Wed, 22 Jun 2005 19:41:19 +0200] rev 16534
tuned;
wenzelm [Wed, 22 Jun 2005 19:41:18 +0200] rev 16533
begin_thy: merge maximal imports;
incorporate proof data;
added generic context;
wenzelm [Wed, 22 Jun 2005 19:41:17 +0200] rev 16532
removed Pure/Isar/proof_data.ML, Pure/General/object.ML;
wenzelm [Wed, 22 Jun 2005 19:41:16 +0200] rev 16531
improved proof;
wenzelm [Wed, 22 Jun 2005 19:41:15 +0200] rev 16530
obsolete (see Pure/context.ML);
wenzelm [Wed, 22 Jun 2005 18:26:28 +0200] rev 16529
tuned;
paulson [Wed, 22 Jun 2005 11:20:45 +0200] rev 16528
pointer equality for sml/nj
haftmann [Wed, 22 Jun 2005 11:09:14 +0200] rev 16527
(initial commit)
haftmann [Wed, 22 Jun 2005 11:08:53 +0200] rev 16526
(initial commit)
haftmann [Wed, 22 Jun 2005 11:07:47 +0200] rev 16525
(initial commit)
haftmann [Wed, 22 Jun 2005 11:07:23 +0200] rev 16524
(initial commit)
nipkow [Wed, 22 Jun 2005 09:26:18 +0200] rev 16523
*** empty log message ***
nipkow [Wed, 22 Jun 2005 07:54:13 +0200] rev 16522
tuned
nipkow [Wed, 22 Jun 2005 07:54:01 +0200] rev 16521
added -H false
quigley [Tue, 21 Jun 2005 23:44:18 +0200] rev 16520
Integrated vampire lemma code.
nipkow [Tue, 21 Jun 2005 21:41:08 +0200] rev 16519
*** empty log message ***
nipkow [Tue, 21 Jun 2005 21:38:27 +0200] rev 16518
added find thms section
wenzelm [Tue, 21 Jun 2005 18:55:57 +0200] rev 16517
proper implementation of pointer_eq;
wenzelm [Tue, 21 Jun 2005 18:55:44 +0200] rev 16516
tuned pointer_eq;
paulson [Tue, 21 Jun 2005 13:34:24 +0200] rev 16515
VAMPIRE_HOME, helper_path and various stylistic tweaks
kleing [Tue, 21 Jun 2005 11:08:31 +0200] rev 16514
lemma, equation between rtrancl and trancl
wenzelm [Tue, 21 Jun 2005 09:51:59 +0200] rev 16513
enter_thms: use theorem database of thy *after* attribute application;
wenzelm [Tue, 21 Jun 2005 09:35:32 +0200] rev 16512
tuned;
wenzelm [Tue, 21 Jun 2005 09:35:31 +0200] rev 16511
added subset, eq_set;
tuned insert/remove: avoid garbage;
wenzelm [Tue, 21 Jun 2005 09:35:30 +0200] rev 16510
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm [Tue, 21 Jun 2005 09:31:57 +0200] rev 16509
fixed HOL-Complex-Matrix target;