X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fmatita.glade;h=75783e6ab0dc16099c6f9fd73b5ce95d72150932;hb=8de1a75899a83dd31e856804bd448c1bd87d9ab3;hp=2b239b4e5485ea3cd93a969023145bd85ca3c6f9;hpb=88f24d23df67d88bf98c2ca32ac0d9854f3d9b00;p=helm.git
diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 2b239b4e5..75783e6ab 100644
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1022,6 +1022,15 @@
True
+
+
+
4
@@ -1464,13 +1504,55 @@
True
True
True
- Top (â¤_i)
0
+
+
+ True
+ Top (â¤<sub>i</sub>)
+ True
+
+
5
+
+
+ True
+ True
+ True
+ 0
+
+
+ True
+ Universal (â<sub>i</sub>)
+ True
+
+
+
+
+ 6
+
+
+
+
+ True
+ True
+ True
+ 0
+
+
+ True
+ Existential (â<sub>i</sub>)
+ True
+
+
+
+
+ 7
+
+
@@ -1499,8 +1581,14 @@
True
True
True
- Implication (â_e)
0
+
+
+ True
+ Implication (â<sub>e</sub>)
+ True
+
+
@@ -1508,8 +1596,14 @@
True
True
True
- Conjunction left (â§_e_l)
0
+
+
+ True
+ Conjunction left (â§<sub>e-l</sub>)
+ True
+
+
1
@@ -1520,8 +1614,14 @@
True
True
True
- Conjunction right (â§_e_r)
0
+
+
+ True
+ Conjunction right (â§<sub>e-r</sub>)
+ True
+
+
2
@@ -1532,8 +1632,14 @@
True
True
True
- Disjunction (â¨_e)
0
+
+
+ True
+ Disjunction (â¨<sub>e</sub>)
+ True
+
+
3
@@ -1544,8 +1650,14 @@
True
True
True
- Negaton (¬_e)
0
+
+
+ True
+ Negation (¬<sub>e</sub>)
+ True
+
+
4
@@ -1556,13 +1668,55 @@
True
True
True
- Bottom (â¥_e)
0
+
+
+ True
+ Bottom (â¥<sub>e</sub>)
+ True
+
+
5
+
+
+ True
+ True
+ True
+ 0
+
+
+ True
+ Universal (â<sub>e</sub>)
+ True
+
+
+
+
+ 6
+
+
+
+
+ True
+ True
+ True
+ 0
+
+
+ True
+ Existential (â<sub>e</sub>)
+ True
+
+
+
+
+ 7
+
+
@@ -1597,17 +1751,29 @@
-
+
True
True
True
- Prove (to start)
+ Use lemma (lem)
0
1
+
+
+ True
+ True
+ True
+ Discharge (discharge)
+ 0
+
+
+ 2
+
+
@@ -2337,6 +2503,59 @@
3
2
5
+
+
+ True
+ 0
+ Find:
+
+
+
+
+
+
+
+
+ True
+ 0
+ Replace with:
+
+
+ 1
+ 2
+
+
+
+
+
+
+ True
+ True
+ True
+ True
+ True
+ *
+
+
+ 1
+ 2
+
+
+
+
+
+ True
+ True
+ *
+
+
+ 1
+ 2
+ 1
+ 2
+
+
+
True
@@ -2435,59 +2654,6 @@
5
-
-
- True
- True
- *
-
-
- 1
- 2
- 1
- 2
-
-
-
-
-
- True
- True
- True
- True
- True
- *
-
-
- 1
- 2
-
-
-
-
-
- True
- 0
- Replace with:
-
-
- 1
- 2
-
-
-
-
-
-
- True
- 0
- Find:
-
-
-
-
-
-