--- a/src/HOL/Lambda/Eta.thy Fri Sep 28 20:09:10 2001 +0200
+++ b/src/HOL/Lambda/Eta.thy Fri Sep 28 21:45:11 2001 +0200
@@ -31,11 +31,11 @@
"s -e>= t" == "(s, t) \<in> eta^="
inductive eta
- intros [simp, intro]
- eta: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
- appL: "s -e> t ==> s $ u -e> t $ u"
- appR: "s -e> t ==> u $ s -e> u $ t"
- abs: "s -e> t ==> Abs s -e> Abs t"
+ intros
+ eta [simp, intro]: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
+ appL [simp, intro]: "s -e> t ==> s $ u -e> t $ u"
+ appR [simp, intro]: "s -e> t ==> u $ s -e> u $ t"
+ abs [simp, intro]: "s -e> t ==> Abs s -e> Abs t"
inductive_cases eta_cases [elim!]:
"Abs s -e> z"
@@ -249,4 +249,4 @@
apply (auto simp add: not_free_iff_lifted)
done
-end
\ No newline at end of file
+end
--- a/src/HOL/Lambda/Lambda.thy Fri Sep 28 20:09:10 2001 +0200
+++ b/src/HOL/Lambda/Lambda.thy Fri Sep 28 21:45:11 2001 +0200
@@ -64,11 +64,11 @@
"s ->> t" == "(s, t) \<in> beta^*"
inductive beta
- intros [simp, intro!]
- beta: "Abs s $ t -> s[t/0]"
- appL: "s -> t ==> s $ u -> t $ u"
- appR: "s -> t ==> u $ s -> u $ t"
- abs: "s -> t ==> Abs s -> Abs t"
+ intros
+ beta [simp, intro!]: "Abs s $ t -> s[t/0]"
+ appL [simp, intro!]: "s -> t ==> s $ u -> t $ u"
+ appR [simp, intro!]: "s -> t ==> u $ s -> u $ t"
+ abs [simp, intro!]: "s -> t ==> Abs s -> Abs t"
inductive_cases beta_cases [elim!]:
"Var i -> t"
@@ -203,4 +203,4 @@
apply (simp add: rtrancl_beta_Abs)
done
-end
\ No newline at end of file
+end
--- a/src/HOL/Lambda/ParRed.thy Fri Sep 28 20:09:10 2001 +0200
+++ b/src/HOL/Lambda/ParRed.thy Fri Sep 28 21:45:11 2001 +0200
@@ -23,11 +23,11 @@
"s => t" == "(s, t) \<in> par_beta"
inductive par_beta
- intros [simp, intro!]
- var: "Var n => Var n"
- abs: "s => t ==> Abs s => Abs t"
- app: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
- beta: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
+ intros
+ var [simp, intro!]: "Var n => Var n"
+ abs [simp, intro!]: "s => t ==> Abs s => Abs t"
+ app [simp, intro!]: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
+ beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
inductive_cases par_beta_cases [elim!]:
"Var n => t"
@@ -130,4 +130,4 @@
par_beta_subset_beta beta_subset_par_beta)+
done
-end
\ No newline at end of file
+end
--- 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