--- 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