--- a/src/HOL/Lambda/Type.thy Fri Sep 28 20:09:10 2001 +0200
+++ b/src/HOL/Lambda/Type.thy Fri Sep 28 21:45:11 2001 +0200
@@ -32,10 +32,10 @@
"Ts =>> T" == "foldr Fun Ts T"
inductive typing
- intros [intro!]
- Var: "env x = T ==> env |- Var x : T"
- Abs: "(nat_case T env) |- t : U ==> env |- Abs t : (T => U)"
- App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
+ intros
+ Var [intro!]: "env x = T ==> env |- Var x : T"
+ Abs [intro!]: "(nat_case T env) |- t : U ==> env |- Abs t : (T => U)"
+ App [intro!]: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
inductive_cases [elim!]:
"e |- Var i : T"
@@ -466,4 +466,4 @@
apply (erule type_implies_IT)
done
-end
\ No newline at end of file
+end