# HG changeset patch
# User wenzelm
# Date 1001706311 -7200
# Node ID 2c3dee321b4b0faa0f4d8bdc144c6da64f9b128c
# Parent  647e6c84323c890c329fc3f634ce827731fdc4a7
inductive: no collective atts;

diff -r 647e6c84323c -r 2c3dee321b4b src/HOL/Lambda/Eta.thy
--- 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
diff -r 647e6c84323c -r 2c3dee321b4b src/HOL/Lambda/Lambda.thy
--- 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
diff -r 647e6c84323c -r 2c3dee321b4b src/HOL/Lambda/ParRed.thy
--- 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
diff -r 647e6c84323c -r 2c3dee321b4b src/HOL/Lambda/Type.thy
--- 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