add comments in some example files.

data61 · Sep 5, 2024 · 731726e · 731726e
1 parent 5edc2d7
commit 731726e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/Example/Abduction_Example/TIP_prop_06.thy b/Example/Abduction_Example/TIP_prop_06.thy
@@ -30,6 +30,7 @@ fun t2 :: "Nat => Nat => Nat" where
   "t2 (Z) z = z"
 | "t2 (S z2) z = S (t2 z2 z)"
 
+(*On a MacBook Pro 2021 or later, this takes about 30 minutes.*)
 prove  property0: "((length (rev (x y z))) = (t2 (length y) (length z)))"
 
 end
diff --git a/Example/Abduction_Example/TIP_prop_11.thy b/Example/Abduction_Example/TIP_prop_11.thy
@@ -20,6 +20,7 @@ fun rev :: "'a list => 'a list" where
   "rev (nil2) = nil2"
 | "rev (cons2 z xs) = x (rev xs) (cons2 z (nil2))"
 
+(*On a MacBook Pro 2021 or later, this takes about 10 minutes.*)
 prove property0 :
   "((rev (x (rev y) (rev z))) = (x z y))"