Commit be8ccf2a authored by MARCHE Claude's avatar MARCHE Claude

restored previous form of example, using _x as variable

parent 917f3e96
......@@ -3,7 +3,7 @@
theory A
type t
axiom Ax : forall x:t. x=x
axiom Ax : forall _x:t. true
end
theory B
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment