- the disambiguation of unified binders continues

[helm.git] / helm / software / helena / examples / grundlagen / grundlagen_2.aut

diff --git a/helm/software/helena/examples/grundlagen/grundlagen_2.aut b/helm/software/helena/examples/grundlagen/grundlagen_2.aut
index 160f840453590652f8630c1894ff9bfcb3917df4..07571ec542d452bf97d91633d5c9b7e8a056029f 100644 (file)
--- a/helm/software/helena/examples/grundlagen/grundlagen_2.aut
+++ b/helm/software/helena/examples/grundlagen/grundlagen_2.aut
@@ -237,6 +237,7 @@ p@[s:sigma][n:not(<s>p)]
 th1:=[x:all(sigma,p)]<<s>x>n:not(all(sigma,p))
 -all
 p@non:=[x:sigma]not(<x>p):[x:sigma]'prop'
+{ to validate }
 some:=not(non(p)):'prop'
 [s:sigma][sp:<s>p]
 somei:=th1".all"(non(p),s,weli(<s>p,sp)):some(sigma,p)
@@ -10715,4 +10716,5 @@ satz301f:=tr3is(real,s,im(pli(r,s)),im(pli(t,u)),u,isim(r,s),isceim(pli(r,s),pli
 -eq
 -st
 -e
+{}
 -l