...

formal topologies

fix some non tex symbols

symbolic links to use the uri manager from ng_kernel

print an error message if graphviz is not found

if gnome-help is not installed, prints an error message

better manual generation

...

one more lazy/loc

according to camlp5 sources, the dummy loc should be 0,0 and not -1,-1

loc * lazy string -> (loc * string) lazy

disambiguation now returns and takes in input the substitution

...

...

...

...

...

dama almost ok

...

...

reverted

dama into the library

x2sx declared as coercion and used when possible

renaming

...

0.5.5

...

...

exercises ready

all ex done

...

....

fixed

removed some printings

commented out unfinished proof

removed some printings

better spacing

apply rule (lem EM) works

missing subst added, now apply rule is probably enough to replace apply

New bug.

no more prove in palette

fixed or-in-left

fixed not-e

Another bug.

This commit shows a bug.

almost ready

rules fixed

make all/clean implemented

housekeeping

housekeeping

house keeping

disambiguation can use a goal as hint for the expected type

natural deduction palette

test 4 luo

...

better names

disambiguation for ng terms almost there

some new exports

new meta added for ng_disambiguation

exported disambiguate_thing

occurr check fixed

more printings

last fixes

1. data structure for lables is now more strict
2. phase 3 completed (with a test)
3. simple optimizer for redundant jumps implemented

- we now use a streaming architecture (run time gain: 11 secs)
- we added some time stamp support

auto-param "size" missing

debug=false

Signature_of has been closed with respect to constructors.

The signature in "retrieve equations" must be extended with the equality if
not already there, otherwise it may hardly find any equation.

some other simplification

ordered_set simplified

exercise ready

exercise ready

almost there

...

First attempts at the third phase.

added some news

almost ok

natural deduction support and example split, seems to almost work.

do not erase sorts

better error messages. sorts are compared using whd

Evil case fixed, the coulde should be more readable

removed empty lines

the passive set and passive list are expected to have the same cardinality, that was was some bad reason not always the case

fixed scripts

still some glitches, but reaching a decent state

using the new by foo we proved semantics

new internal flags for auto:
- skip_context
- skip_trie_filtering

together they allow a decent semantics for
by H, H1, H2 we proved foo.

since only H, H1 and H2 are used (no other context entry, not library stuff)
and full blown unification is used (no terms are ignored, between the one
specified, because they fail a trie search)

duplicate entry in menv avoided

fixed script to use auto depth=4

eliminazione di un passaggio di transitività in ast2astfe
dimostrazione di un assioma in env2flatenv

Calling unification instead of matching when checking for subsumption
might instantiate the goal with variables in table (while they are supposed
to be disjoint).

- A new interesting elimination principle over inductively generated topologies:
  the elimination principle for general topologies hold!
- A proof of Cantor theorem using formal topologies. By Silvio Valentini.

BDD

removed prerr_endline

debug=false

shannon proved

added shannon

added lazy

Environment simplified.