Thu, 23 Jun 2005 22:10:29 +0200 add binder syntax for flift1
huffman [Thu, 23 Jun 2005 22:10:29 +0200] rev 16555
add binder syntax for flift1
Thu, 23 Jun 2005 22:08:24 +0200 add new file to test fixrec package
huffman [Thu, 23 Jun 2005 22:08:24 +0200] rev 16554
add new file to test fixrec package
Thu, 23 Jun 2005 22:07:30 +0200 add csplit3, ssplit3, fup3 as simp rules
huffman [Thu, 23 Jun 2005 22:07:30 +0200] rev 16553
add csplit3, ssplit3, fup3 as simp rules
Thu, 23 Jun 2005 21:27:23 +0200 New features:
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
Thu, 23 Jun 2005 21:17:26 +0200 added match functions for spair, sinl, sinr
huffman [Thu, 23 Jun 2005 21:17:26 +0200] rev 16551
added match functions for spair, sinl, sinr
Thu, 23 Jun 2005 19:40:03 +0200 fixed \<Prod> syntax
nipkow [Thu, 23 Jun 2005 19:40:03 +0200] rev 16550
fixed \<Prod> syntax
Thu, 23 Jun 2005 07:32:59 +0200 new
nipkow [Thu, 23 Jun 2005 07:32:59 +0200] rev 16549
new
Wed, 22 Jun 2005 20:26:31 +0200 Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
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.
Wed, 22 Jun 2005 19:48:20 +0200 * Pure: the Isar proof context type is already defined early in Pure
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;
Wed, 22 Jun 2005 19:44:12 +0200 added find2
nipkow [Wed, 22 Jun 2005 19:44:12 +0200] rev 16546
added find2
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip