kleing [Wed, 17 Nov 2004 07:35:50 +0100] rev 15291
removed Exercises document (available on separate web site now)
kleing [Wed, 17 Nov 2004 07:35:14 +0100] rev 15290
removed exercised document
aspinall [Tue, 16 Nov 2004 20:20:14 +0100] rev 15289
Markup obtain as introducing a nested goal.
paulson [Mon, 15 Nov 2004 18:21:34 +0100] rev 15288
removed a "clone" (duplicate code)
webertj [Mon, 15 Nov 2004 17:04:11 +0100] rev 15287
minor rewording
aspinall [Mon, 15 Nov 2004 13:51:43 +0100] rev 15286
Add <undoitem> for theory-state undos.
paulson [Mon, 15 Nov 2004 12:13:14 +0100] rev 15285
Renamed some variables to eliminate conflicts with constants.
Introduced some abbreviations (following TPTP axiom sets) to reduce the
amount of repetition.
Uncommented some examples, which increases the runtime somewhat.
webertj [Sun, 14 Nov 2004 01:56:58 +0100] rev 15284
*** empty log message ***
webertj [Sun, 14 Nov 2004 01:40:27 +0100] rev 15283
DOCTYPE declaration added
webertj [Sat, 13 Nov 2004 17:30:03 +0100] rev 15282
Exercises added
nipkow [Sat, 13 Nov 2004 07:47:34 +0100] rev 15281
More lemmas
webertj [Fri, 12 Nov 2004 20:55:04 +0100] rev 15280
minor code refactoring
paulson [Fri, 12 Nov 2004 16:26:19 +0100] rev 15279
improved "subscribe" link
webertj [Fri, 12 Nov 2004 15:49:25 +0100] rev 15278
added DOCTYPE and Content-Type declarations to make this a valid HTML file
webertj [Fri, 12 Nov 2004 15:45:19 +0100] rev 15277
isatool usedir -f
paulson [Thu, 11 Nov 2004 10:50:24 +0100] rev 15276
updated subscription wording and link
paulson [Thu, 11 Nov 2004 10:26:40 +0100] rev 15275
increased tracing and search bounds
paulson [Mon, 08 Nov 2004 16:53:50 +0100] rev 15274
tidied comments
schirmer [Fri, 05 Nov 2004 15:37:25 +0100] rev 15273
* extended interface of record_split_simp_tac and record_split_simproc
* improved record_type_abbr_tr'
chaieb [Tue, 02 Nov 2004 16:33:08 +0100] rev 15272
user-interface impoved
paulson [Fri, 29 Oct 2004 15:16:31 +0200] rev 15271
fixed some awkward problems with nat/int simprocs
paulson [Fri, 29 Oct 2004 15:16:02 +0200] rev 15270
fixed reference to renamed theorem
webertj [Thu, 28 Oct 2004 19:40:22 +0200] rev 15269
isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)
aspinall [Thu, 28 Oct 2004 17:11:51 +0200] rev 15268
Make <undostep> call undos_proof to display resulting proofstate.
chaieb [Thu, 28 Oct 2004 11:58:22 +0200] rev 15267
efficienty improvement
Heuristic is now the same as for the proof-generating alg.
aspinall [Wed, 27 Oct 2004 19:45:16 +0200] rev 15266
Revert change to pgml_sym
berghofe [Wed, 27 Oct 2004 10:30:07 +0200] rev 15265
Added type constraint to make SML/NJ happy.
berghofe [Tue, 26 Oct 2004 16:34:19 +0200] rev 15264
Changed function cabs to also allow abstraction over Vars.
berghofe [Tue, 26 Oct 2004 16:33:35 +0200] rev 15263
Added function merge_alists'.
berghofe [Tue, 26 Oct 2004 16:33:09 +0200] rev 15262
Added function strip_type (for ctyps).
berghofe [Tue, 26 Oct 2004 16:32:09 +0200] rev 15261
Added preprocessors.
berghofe [Tue, 26 Oct 2004 16:31:09 +0200] rev 15260
Added setup for code generator.
berghofe [Tue, 26 Oct 2004 16:30:32 +0200] rev 15259
Added simple code generator.
berghofe [Tue, 26 Oct 2004 16:29:54 +0200] rev 15258
Removed code generator stuff. Code generation is now handled by code
generator in typedef_package.
berghofe [Tue, 26 Oct 2004 16:26:53 +0200] rev 15257
Added call to Codegen.preprocess.
berghofe [Tue, 26 Oct 2004 16:25:41 +0200] rev 15256
Fixed problem with sorts in function make_casedists.
nipkow [Mon, 25 Oct 2004 17:19:17 +0200] rev 15255
fixed urls
aspinall [Sun, 24 Oct 2004 15:41:52 +0200] rev 15254
Simplification to symbol processing; put quotes around theory name in message.
aspinall [Thu, 21 Oct 2004 19:21:32 +0200] rev 15253
Fix <closetheory>
berghofe [Tue, 19 Oct 2004 22:45:20 +0200] rev 15252
Replaced PolyML specific print function by Display.print_thm(s)
paulson [Tue, 19 Oct 2004 18:18:45 +0200] rev 15251
converted some induct_tac to induct
dixon [Mon, 18 Oct 2004 13:40:45 +0200] rev 15250
added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
berghofe [Mon, 18 Oct 2004 11:43:40 +0200] rev 15249
Replaced list of bound variables in simpset by maximal index of bound
variables. This allows new variable names to be generated more quickly
(without calling variant).
schirmer [Fri, 15 Oct 2004 18:49:16 +0200] rev 15248
record_split_simp_tac now can get simp rules as parameter
nipkow [Fri, 15 Oct 2004 18:16:11 +0200] rev 15247
update
nipkow [Fri, 15 Oct 2004 18:16:03 +0200] rev 15246
added and renamed
nipkow [Thu, 14 Oct 2004 12:18:52 +0200] rev 15245
Added a few lemmas
nipkow [Wed, 13 Oct 2004 07:40:13 +0200] rev 15244
mod becuase of chnage in induct