Relación 4 - Historial de revisiones

WikiSysop: Texto reemplazado: «"isar"» por «"isabelle"»

2018-07-16T08:23:19Z

Texto reemplazado: «"isar"» por «"isabelle"»

2014-11-20T15:02:30Z

2014-11-20T14:09:25Z

2014-11-20T10:12:31Z

2014-11-17T08:48:37Z

2014-11-16T20:57:40Z

2014-11-16T18:35:13Z

2014-11-16T18:34:55Z

2014-11-15T11:05:41Z

2014-11-14T17:09:15Z

@@ Línea 18: / Línea 18: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom, carvelcab"
 fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
@@ Línea 31: / Línea 31: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom, carvelcab"
 lemma "snoc xs a = xs @ [a]"
@@ Línea 45: / Línea 45: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom, carvelcab"
 lemma snoc_append: "snoc xs a = xs @ [a]"
@@ Línea 75: / Línea 75: @@
 lemma "rev (x # xs) = snoc (rev xs) x"
 by (simp add: snoc_append)
 text {*
@@ Línea 83: / Línea 87: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, juacorvic, marnajgom, domcadgom"
+-- "davoremar,javrodviv1, jeshorcob, juacorvic, marnajgom, domcadgom, carvelcab"
 lemma "rev (x # xs) = snoc (rev xs) x"

@@ Línea 18: / Línea 18: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom"
 fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
@@ Línea 31: / Línea 31: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom"
 lemma "snoc xs a = xs @ [a]"
@@ Línea 45: / Línea 45: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom"
 lemma snoc_append: "snoc xs a = xs @ [a]"
@@ Línea 72: / Línea 72: @@
 (*Pedrosrei:no hace falta usar auto, sirve simp*)
--- "juacorvic"
+-- "juacorvic, domcadgom"
 lemma "rev (x # xs) = snoc (rev xs) x"
 by (simp add: snoc_append)
@@ Línea 83: / Línea 83: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, juacorvic, marnajgom"
+-- "davoremar,javrodviv1, jeshorcob, juacorvic, marnajgom, domcadgom"
 lemma "rev (x # xs) = snoc (rev xs) x"

@@ Línea 18: / Línea 18: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom"
 fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
@@ Línea 31: / Línea 31: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom"
 lemma "snoc xs a = xs @ [a]"
@@ Línea 45: / Línea 45: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom"
 lemma snoc_append: "snoc xs a = xs @ [a]"
@@ Línea 65: / Línea 65: @@
 *}
--- "davoremar,javrodviv1, jeshorcob"
+-- "davoremar,javrodviv1, jeshorcob, marnajgom"
 lemma "rev (x # xs) = snoc (rev xs) x"
@@ Línea 83: / Línea 83: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, juacorvic"
+-- "davoremar,javrodviv1, jeshorcob, juacorvic, marnajgom"
 lemma "rev (x # xs) = snoc (rev xs) x"

@@ Línea 18: / Línea 18: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic"
 fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
@@ Línea 31: / Línea 31: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic"
 lemma "snoc xs a = xs @ [a]"
@@ Línea 45: / Línea 45: @@
 *}
--- "davoremar,javrodviv1, jeshorcob, emimarriv"
+-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic"
 lemma snoc_append: "snoc xs a = xs @ [a]"
@@ Línea 71: / Línea 71: @@
 (*Pedrosrei:no hace falta usar auto, sirve simp*)
 text {*
@@ Línea 79: / Línea 83: @@
 *}
--- "davoremar,javrodviv1, jeshorcob"
+-- "davoremar,javrodviv1, jeshorcob, juacorvic"
 lemma "rev (x # xs) = snoc (rev xs) x"

@@ Línea 36: / Línea 36: @@
 by (induct xs) auto
-(*Pedrosrei:no hace falta usar, sirve simp_all*)
+(*Pedrosrei:no hace falta usar auto, sirve simp_all*)
 text {*

@@ Línea 18: / Línea 18: @@
 *}
--- "davoremar"
+-- "davoremar,javrodviv1"
 fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
@@ Línea 31: / Línea 31: @@
 *}
--- "davoremar"
+-- "davoremar,javrodviv1"
 lemma "snoc xs a = xs @ [a]"
@@ Línea 43: / Línea 43: @@
 *}
--- "davoremar"
+-- "davoremar,javrodviv1"
 lemma snoc_append: "snoc xs a = xs @ [a]"
@@ Línea 63: / Línea 63: @@
 *}
--- "davoremar"
+-- "davoremar,javrodviv1"
 lemma "rev (x # xs) = snoc (rev xs) x"
@@ Línea 75: / Línea 75: @@
 *}
--- "davoremar"
+-- "davoremar,javrodviv1"
 lemma "rev (x # xs) = snoc (rev xs) x"