Changeset 2474 for src/joint

Timestamp:

Nov 19, 2012, 10:57:08 AM (9 years ago)

Author:

tranquil

Message:

changed form of a statement

File:

• src/joint/linearise.ma (modified) (2 diffs)

src/joint/linearise.ma

@@ -173 +173 @@
     ] n_prf
   ] (chop_ok ? (λx.x∈visited) visiting).
+(*cases daemon qed. *)
 whd
 [ (* base case, visiting is all visited *)
@@ -746 +747 @@
     \snd (linearise_int_fun … fn_in))
 %{sigma}
-* #i #i_prf >(prog_if_of_function_transform … i_prf)
+#i >(prog_if_of_function_transform … i) [2: % ] 
 normalize nodelta
 cases (linearise_int_fun ???) * #fn_out #sigma_loc