author wenzelm Fri, 25 Nov 2005 18:58:34 +0100 changeset 18248 929659a46ecf parent 18247 b17724cae935 child 18249 4398f0f12579
tuned;
 NEWS file | annotate | diff | comparison | revisions src/Pure/logic.ML file | annotate | diff | comparison | revisions
```--- a/NEWS	Fri Nov 25 17:41:52 2005 +0100
+++ b/NEWS	Fri Nov 25 18:58:34 2005 +0100
@@ -78,10 +78,10 @@
shows "P n x"
using a                     -- {* make induct insert fact a *}
proof (induct n fixing: x)    -- {* generalize goal to "!!x. A n x ==> P n x" *}
-    case (0 x)
+    case 0
show ?case sorry
next
-    case (Suc n x)
+    case (Suc n)
note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *}
note `A (Suc n) x`          -- {* induction premise, stemming from fact a *}
show ?case sorry```
```--- a/src/Pure/logic.ML	Fri Nov 25 17:41:52 2005 +0100
+++ b/src/Pure/logic.ML	Fri Nov 25 18:58:34 2005 +0100
@@ -229,21 +229,21 @@
end;

-(*Make lifting functions from subgoal and increment.
+(* Lifting functions from subgoal and increment:
lift_abs operates on terms
lift_all operates on propositions *)

fun lift_abs inc =
let
fun lift Ts (Const ("==>", _) \$ _ \$ B) t = lift Ts B t
-      | lift Ts (Const ("all", _) \$ Abs (a, T, b)) t = Abs (a, T, lift (T :: Ts) b t)
+      | lift Ts (Const ("all", _) \$ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
| lift Ts _ t = incr_indexes (rev Ts, inc) t;
in lift [] end;

fun lift_all inc =
let
fun lift Ts ((c as Const ("==>", _)) \$ A \$ B) t = c \$ A \$ lift Ts B t
-      | lift Ts ((c as Const ("all", _)) \$ Abs (a, T, b)) t = c \$ Abs (a, T, lift (T :: Ts) b t)
+      | lift Ts ((c as Const ("all", _)) \$ Abs (a, T, B)) t = c \$ Abs (a, T, lift (T :: Ts) B t)
| lift Ts _ t = incr_indexes (rev Ts, inc) t;
in lift [] end;
```