src/HOL/Lambda/ParRed.thy
changeset 11638 2c3dee321b4b
parent 9941 fe05af7ec816
child 12011 1a3a7b3cd9bb
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Fri Sep 28 20:09:10 2001 +0200
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Fri Sep 28 21:45:11 2001 +0200
     1.3 @@ -23,11 +23,11 @@
     1.4    "s => t" == "(s, t) \<in> par_beta"
     1.5  
     1.6  inductive par_beta
     1.7 -  intros [simp, intro!]
     1.8 -    var: "Var n => Var n"
     1.9 -    abs: "s => t ==> Abs s => Abs t"
    1.10 -    app: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
    1.11 -    beta: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
    1.12 +  intros
    1.13 +    var [simp, intro!]: "Var n => Var n"
    1.14 +    abs [simp, intro!]: "s => t ==> Abs s => Abs t"
    1.15 +    app [simp, intro!]: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
    1.16 +    beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
    1.17  
    1.18  inductive_cases par_beta_cases [elim!]:
    1.19    "Var n => t"
    1.20 @@ -130,4 +130,4 @@
    1.21      par_beta_subset_beta beta_subset_par_beta)+
    1.22    done
    1.23  
    1.24 -end
    1.25 \ No newline at end of file
    1.26 +end