wenzelm [Wed, 29 Jun 2005 15:13:30 +0200] rev 16600
Syntax.read thy;
wenzelm [Wed, 29 Jun 2005 15:13:29 +0200] rev 16599
tuned sort_ord: pointer_eq;
tuned size_of_term: less stack usage;
wenzelm [Wed, 29 Jun 2005 15:13:28 +0200] rev 16598
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
added efficient operations on ordered lists: eq_set, union, subtract, insert_sort/typ(s)/term(s);
wenzelm [Wed, 29 Jun 2005 15:13:27 +0200] rev 16597
eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;
wenzelm [Wed, 29 Jun 2005 15:13:26 +0200] rev 16596
replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);
wenzelm [Wed, 29 Jun 2005 15:13:25 +0200] rev 16595
added implies_intr_hyps (from thm.ML);
wenzelm [Wed, 29 Jun 2005 15:13:23 +0200] rev 16594
added joinable;
paulson [Tue, 28 Jun 2005 17:56:04 +0200] rev 16593
stylistic improvements
haftmann [Tue, 28 Jun 2005 16:12:03 +0200] rev 16592
added project information in overview
haftmann [Tue, 28 Jun 2005 16:12:03 +0200] rev 16591
added project information in overview
haftmann [Tue, 28 Jun 2005 15:47:50 +0200] rev 16590
more sophisticated pypager
paulson [Tue, 28 Jun 2005 15:28:30 +0200] rev 16589
first-order check now allows quantifiers
paulson [Tue, 28 Jun 2005 15:28:04 +0200] rev 16588
stricter first-order check for meson
paulson [Tue, 28 Jun 2005 15:27:45 +0200] rev 16587
Constant "If" is now local
haftmann [Tue, 28 Jun 2005 15:26:45 +0200] rev 16586
more sophisticated pypager
paulson [Tue, 28 Jun 2005 15:26:32 +0200] rev 16585
replacing zabs_def by abs_if
haftmann [Tue, 28 Jun 2005 12:32:38 +0200] rev 16584
introduced a notion of mirrors
haftmann [Tue, 28 Jun 2005 12:25:19 +0200] rev 16583
some minor improvements
haftmann [Tue, 28 Jun 2005 12:25:19 +0200] rev 16582
some minor improvements
haftmann [Tue, 28 Jun 2005 12:16:01 +0200] rev 16581
some minor improvements
haftmann [Tue, 28 Jun 2005 12:16:01 +0200] rev 16580
some minor improvements
haftmann [Tue, 28 Jun 2005 12:03:43 +0200] rev 16579
some minor improvements
haftmann [Tue, 28 Jun 2005 12:03:19 +0200] rev 16578
some minor improvements
haftmann [Tue, 28 Jun 2005 11:59:38 +0200] rev 16577
some minor improvements
haftmann [Tue, 28 Jun 2005 11:58:56 +0200] rev 16576
some minor improvements
haftmann [Tue, 28 Jun 2005 11:55:30 +0200] rev 16575
some minor improvements
haftmann [Tue, 28 Jun 2005 11:55:30 +0200] rev 16574
some minor improvements
haftmann [Tue, 28 Jun 2005 10:24:53 +0200] rev 16573
corrected comment
haftmann [Tue, 28 Jun 2005 09:41:39 +0200] rev 16572
some corrections
wenzelm [Sun, 26 Jun 2005 15:16:58 +0200] rev 16571
export get_calculation;
nipkow [Sat, 25 Jun 2005 16:07:55 +0200] rev 16570
Added term_lpo
nipkow [Sat, 25 Jun 2005 16:07:13 +0200] rev 16569
cancels completely within terms as well now.
nipkow [Sat, 25 Jun 2005 16:06:17 +0200] rev 16568
Changes due to new abel_cancel.ML
kleing [Sat, 25 Jun 2005 12:37:07 +0200] rev 16567
use both processors on macbroy5
kleing [Sat, 25 Jun 2005 02:43:43 +0200] rev 16566
switch mac test to macbroy5
huffman [Sat, 25 Jun 2005 01:09:14 +0200] rev 16565
cleaned up
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 ***