]> matita.cs.unibo.it Git - helm.git/commit
update in ground and delayed updating
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 8 Jan 2022 20:09:45 +0000 (21:09 +0100)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 8 Jan 2022 20:09:45 +0000 (21:09 +0100)
commitcc178d85bc4fec05b6a9dd176f338b3275beb3d9
treed4a36f0a3ca8e232627eb5290abfbbc4090a7bc6
parent5489d0b66ed7bff17b9dedb89708f57f1d542adc
update in ground and delayed updating

+ notation at level 75 moved at level 70
+ dfr, ifr: path depth was not considered
53 files changed:
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_a_0.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_l_0.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_s_0.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_1.ma
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma
matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground/lib/list_length.ma
matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma
matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/circled_element_e_1.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonleft_2.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonright_2.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonrightstar_3.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_1.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_2.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/element_b_2.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/element_e_0.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/element_i_0.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/element_t_1.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/element_u_1.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/verticalbars_1.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat_id.ma
matita/matita/predefined_virtuals.ml