src/HOL/TLA/Action.thy
changeset 27104 791607529f6d
parent 24180 9f818139951b
child 30528 7173bf123335
     1.1 --- a/src/HOL/TLA/Action.thy	Tue Jun 10 15:30:06 2008 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Tue Jun 10 15:30:33 2008 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4  lemma actionI [intro!]:
     1.5    assumes "!!s t. (s,t) |= A"
     1.6    shows "|- A"
     1.7 -  apply (rule assms intI prod_induct)+
     1.8 +  apply (rule assms intI prod.induct)+
     1.9    done
    1.10  
    1.11  lemma actionD [dest]: "|- A ==> (s,t) |= A"