matita.cs.unibo.it Git - helm.git/tree - matita/matita/contribs/lambdadelta/ground/relocation/

drwxr-xr-x		..
-rw-r--r--	1780	fr2_append.ma	blob \| history \| raw
-rw-r--r--	1577	fr2_map.ma	blob \| history \| raw
-rw-r--r--	3220	fr2_minus.ma	blob \| history \| raw
-rw-r--r--	3059	fr2_nat.ma	blob \| history \| raw
-rw-r--r--	1618	fr2_nat_nat.ma	blob \| history \| raw
-rw-r--r--	2172	fr2_plus.ma	blob \| history \| raw
-rw-r--r--	2612	nap.ma	blob \| history \| raw
-rw-r--r--	7421	pr_after.ma	blob \| history \| raw
-rw-r--r--	3873	pr_after_after.ma	blob \| history \| raw
-rw-r--r--	2937	pr_after_after_ist.ma	blob \| history \| raw
-rw-r--r--	1855	pr_after_basic.ma	blob \| history \| raw
-rw-r--r--	3142	pr_after_eq.ma	blob \| history \| raw
-rw-r--r--	2973	pr_after_isi.ma	blob \| history \| raw
-rw-r--r--	3080	pr_after_ist.ma	blob \| history \| raw
-rw-r--r--	2033	pr_after_ist_isi.ma	blob \| history \| raw
-rw-r--r--	1829	pr_after_isu.ma	blob \| history \| raw
-rw-r--r--	2159	pr_after_nat.ma	blob \| history \| raw
-rw-r--r--	2808	pr_after_nat_uni_tls.ma	blob \| history \| raw
-rw-r--r--	4127	pr_after_pat.ma	blob \| history \| raw
-rw-r--r--	1718	pr_after_pat_tls.ma	blob \| history \| raw
-rw-r--r--	3547	pr_after_pat_uni_tls.ma	blob \| history \| raw
-rw-r--r--	2397	pr_after_uni.ma	blob \| history \| raw
-rw-r--r--	1696	pr_basic.ma	blob \| history \| raw
-rw-r--r--	8587	pr_coafter.ma	blob \| history \| raw
-rw-r--r--	1940	pr_coafter_coafter.ma	blob \| history \| raw
-rw-r--r--	2946	pr_coafter_coafter_ist.ma	blob \| history \| raw
-rw-r--r--	3198	pr_coafter_eq.ma	blob \| history \| raw
-rw-r--r--	2264	pr_coafter_isi.ma	blob \| history \| raw
-rw-r--r--	3015	pr_coafter_ist_isf.ma	blob \| history \| raw
-rw-r--r--	2894	pr_coafter_ist_isi.ma	blob \| history \| raw
-rw-r--r--	1586	pr_coafter_isu.ma	blob \| history \| raw
-rw-r--r--	2340	pr_coafter_nat_tls.ma	blob \| history \| raw
-rw-r--r--	2288	pr_coafter_nat_tls_pushs.ma	blob \| history \| raw
-rw-r--r--	2849	pr_coafter_pat_tls.ma	blob \| history \| raw
-rw-r--r--	1516	pr_coafter_uni_pushs.ma	blob \| history \| raw
-rw-r--r--	2522	pr_compose.ma	blob \| history \| raw
-rw-r--r--	2832	pr_eq.ma	blob \| history \| raw
-rw-r--r--	3285	pr_fcla.ma	blob \| history \| raw
-rw-r--r--	1733	pr_fcla_eq.ma	blob \| history \| raw
-rw-r--r--	1517	pr_fcla_fcla.ma	blob \| history \| raw
-rw-r--r--	1389	pr_fcla_uni.ma	blob \| history \| raw
-rw-r--r--	1502	pr_id.ma	blob \| history \| raw
-rw-r--r--	1798	pr_id_eq.ma	blob \| history \| raw
-rw-r--r--	2104	pr_isd.ma	blob \| history \| raw
-rw-r--r--	2316	pr_isd_eq.ma	blob \| history \| raw
-rw-r--r--	1625	pr_isd_nexts.ma	blob \| history \| raw
-rw-r--r--	1421	pr_isd_tl.ma	blob \| history \| raw
-rw-r--r--	1382	pr_isd_tls.ma	blob \| history \| raw
-rw-r--r--	2624	pr_isf.ma	blob \| history \| raw
-rw-r--r--	1528	pr_isf_eq.ma	blob \| history \| raw
-rw-r--r--	1376	pr_isf_isu.ma	blob \| history \| raw
-rw-r--r--	1625	pr_isf_pushs.ma	blob \| history \| raw
-rw-r--r--	1636	pr_isf_tl.ma	blob \| history \| raw
-rw-r--r--	1596	pr_isf_tls.ma	blob \| history \| raw
-rw-r--r--	1338	pr_isf_uni.ma	blob \| history \| raw
-rw-r--r--	2087	pr_isi.ma	blob \| history \| raw
-rw-r--r--	2311	pr_isi_eq.ma	blob \| history \| raw
-rw-r--r--	1639	pr_isi_id.ma	blob \| history \| raw
-rw-r--r--	1752	pr_isi_nat.ma	blob \| history \| raw
-rw-r--r--	1892	pr_isi_pat.ma	blob \| history \| raw
-rw-r--r--	1623	pr_isi_pushs.ma	blob \| history \| raw
-rw-r--r--	1420	pr_isi_tl.ma	blob \| history \| raw
-rw-r--r--	1381	pr_isi_tls.ma	blob \| history \| raw
-rw-r--r--	1578	pr_isi_uni.ma	blob \| history \| raw
-rw-r--r--	2496	pr_ist.ma	blob \| history \| raw
-rw-r--r--	1477	pr_ist_isi.ma	blob \| history \| raw
-rw-r--r--	3494	pr_ist_ist.ma	blob \| history \| raw
-rw-r--r--	1409	pr_ist_tls.ma	blob \| history \| raw
-rw-r--r--	2219	pr_isu.ma	blob \| history \| raw
-rw-r--r--	1750	pr_isu_tl.ma	blob \| history \| raw
-rw-r--r--	2035	pr_isu_uni.ma	blob \| history \| raw
-rw-r--r--	2425	pr_map.ma	blob \| history \| raw
-rw-r--r--	8053	pr_nat.ma	blob \| history \| raw
-rw-r--r--	2195	pr_nat_basic.ma	blob \| history \| raw
-rw-r--r--	3227	pr_nat_nat.ma	blob \| history \| raw
-rw-r--r--	1590	pr_nat_uni.ma	blob \| history \| raw
-rw-r--r--	1888	pr_nexts.ma	blob \| history \| raw
-rw-r--r--	2130	pr_nexts_eq.ma	blob \| history \| raw
-rw-r--r--	7817	pr_pat.ma	blob \| history \| raw
-rw-r--r--	2060	pr_pat_basic.ma	blob \| history \| raw
-rw-r--r--	2445	pr_pat_eq.ma	blob \| history \| raw
-rw-r--r--	1570	pr_pat_id.ma	blob \| history \| raw
-rw-r--r--	3296	pr_pat_lt.ma	blob \| history \| raw
-rw-r--r--	5005	pr_pat_pat.ma	blob \| history \| raw
-rw-r--r--	1795	pr_pat_pat_id.ma	blob \| history \| raw
-rw-r--r--	3273	pr_pat_tls.ma	blob \| history \| raw
-rw-r--r--	1650	pr_pat_uni.ma	blob \| history \| raw
-rw-r--r--	1887	pr_pushs.ma	blob \| history \| raw
-rw-r--r--	1407	pr_pushs_eq.ma	blob \| history \| raw
-rw-r--r--	4976	pr_sand.ma	blob \| history \| raw
-rw-r--r--	2933	pr_sand_eq.ma	blob \| history \| raw
-rw-r--r--	4990	pr_sdj.ma	blob \| history \| raw
-rw-r--r--	2422	pr_sdj_eq.ma	blob \| history \| raw
-rw-r--r--	2009	pr_sdj_isi.ma	blob \| history \| raw
-rw-r--r--	5453	pr_sle.ma	blob \| history \| raw
-rw-r--r--	2566	pr_sle_eq.ma	blob \| history \| raw
-rw-r--r--	1807	pr_sle_isd.ma	blob \| history \| raw
-rw-r--r--	1805	pr_sle_isi.ma	blob \| history \| raw
-rw-r--r--	1418	pr_sle_pushs.ma	blob \| history \| raw
-rw-r--r--	1486	pr_sle_sle.ma	blob \| history \| raw
-rw-r--r--	1410	pr_sle_tls.ma	blob \| history \| raw
-rw-r--r--	12350	pr_sor.ma	blob \| history \| raw
-rw-r--r--	4025	pr_sor_coafter_ist_isf.ma	blob \| history \| raw
-rw-r--r--	2908	pr_sor_eq.ma	blob \| history \| raw
-rw-r--r--	3577	pr_sor_fcla.ma	blob \| history \| raw
-rw-r--r--	2563	pr_sor_isf.ma	blob \| history \| raw
-rw-r--r--	3204	pr_sor_isi.ma	blob \| history \| raw
-rw-r--r--	2645	pr_sor_sle.ma	blob \| history \| raw
-rw-r--r--	5760	pr_sor_sor.ma	blob \| history \| raw
-rw-r--r--	1416	pr_sor_sor_sle.ma	blob \| history \| raw
-rw-r--r--	1436	pr_sor_tls.ma	blob \| history \| raw
-rw-r--r--	1766	pr_tl.ma	blob \| history \| raw
-rw-r--r--	4082	pr_tl_eq.ma	blob \| history \| raw
-rw-r--r--	1710	pr_tl_eq_eq.ma	blob \| history \| raw
-rw-r--r--	1806	pr_tls.ma	blob \| history \| raw
-rw-r--r--	1406	pr_tls_eq.ma	blob \| history \| raw
-rw-r--r--	1933	pr_tls_nexts_eq.ma	blob \| history \| raw
-rw-r--r--	1401	pr_tls_pushs.ma	blob \| history \| raw
-rw-r--r--	1933	pr_tls_pushs_eq.ma	blob \| history \| raw
-rw-r--r--	1613	pr_uni.ma	blob \| history \| raw
-rw-r--r--	2551	pr_uni_eq.ma	blob \| history \| raw
-rw-r--r--	2312	tr_compose.ma	blob \| history \| raw
-rw-r--r--	1548	tr_compose_compose.ma	blob \| history \| raw
-rw-r--r--	1615	tr_compose_eq.ma	blob \| history \| raw
-rw-r--r--	5393	tr_compose_etc.ma	blob \| history \| raw
-rw-r--r--	1548	tr_compose_pap.ma	blob \| history \| raw
-rw-r--r--	2534	tr_compose_pn.ma	blob \| history \| raw
-rw-r--r--	1464	tr_compose_pushs.ma	blob \| history \| raw
-rw-r--r--	1633	tr_compose_tls.ma	blob \| history \| raw
-rw-r--r--	1848	tr_eq.ma	blob \| history \| raw
-rw-r--r--	1473	tr_id.ma	blob \| history \| raw
-rw-r--r--	1463	tr_id_compose.ma	blob \| history \| raw
-rw-r--r--	1421	tr_id_hdtl.ma	blob \| history \| raw
-rw-r--r--	1358	tr_id_pap.ma	blob \| history \| raw
-rw-r--r--	1346	tr_id_pushs.ma	blob \| history \| raw
-rw-r--r--	1354	tr_id_tls.ma	blob \| history \| raw
-rw-r--r--	1332	tr_ist.ma	blob \| history \| raw
-rw-r--r--	3022	tr_map.ma	blob \| history \| raw
-rw-r--r--	1477	tr_nexts.ma	blob \| history \| raw
-rw-r--r--	1758	tr_pap.ma	blob \| history \| raw
-rw-r--r--	2021	tr_pap_eq.ma	blob \| history \| raw
-rw-r--r--	1310	tr_pap_hdtl.ma	blob \| history \| raw
-rw-r--r--	1430	tr_pap_hdtl_eq.ma	blob \| history \| raw
-rw-r--r--	1347	tr_pap_lt.ma	blob \| history \| raw
-rw-r--r--	1357	tr_pap_pap.ma	blob \| history \| raw
-rw-r--r--	1688	tr_pap_pat.ma	blob \| history \| raw
-rw-r--r--	1523	tr_pap_pn.ma	blob \| history \| raw
-rw-r--r--	1631	tr_pap_pushs.ma	blob \| history \| raw
-rw-r--r--	1480	tr_pap_tls.ma	blob \| history \| raw
-rw-r--r--	3240	tr_pat.ma	blob \| history \| raw
-rw-r--r--	2044	tr_pn.ma	blob \| history \| raw
-rw-r--r--	1533	tr_pn_eq.ma	blob \| history \| raw
-rw-r--r--	1374	tr_pn_hdtl.ma	blob \| history \| raw
-rw-r--r--	1429	tr_pn_tls.ma	blob \| history \| raw
-rw-r--r--	1803	tr_pushs.ma	blob \| history \| raw
-rw-r--r--	1431	tr_pushs_tls.ma	blob \| history \| raw
-rw-r--r--	1624	tr_uni.ma	blob \| history \| raw
-rw-r--r--	2510	tr_uni_compose.ma	blob \| history \| raw
-rw-r--r--	1326	tr_uni_eq.ma	blob \| history \| raw
-rw-r--r--	1438	tr_uni_hdtl.ma	blob \| history \| raw
-rw-r--r--	1486	tr_uni_pap.ma	blob \| history \| raw
-rw-r--r--	1326	tr_uni_tls.ma	blob \| history \| raw
-rw-r--r--	2200	xap.ma	blob \| history \| raw