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.