Index: plsrc/nat_spec_demo.pl
==================================================================
--- plsrc/nat_spec_demo.pl
+++ plsrc/nat_spec_demo.pl
@@ -11,11 +11,11 @@
% Due to an oversight on my part, the way we handle inductive proofs,
% although correct, will not work with the kind of incremental proofs
% construction we are aiming to do. More permanent solutions will have to
% come later, but for now we hard-code the IH into the specification.
% (Which, yes, means that you can only prove one thing by induction!)
- ih('IH', add(' x', z, ' x'), 'nat\\sml'(' x')),
+ ih('IH', add(' x', z, ' x'), 'nat|sml'(' x')),
% Nat formation rules
rule('Nat-z', nat(z), and([true])),
rule('Nat-succ', nat(s(' n')), and([nat(' n')])),