To be consistent with "induct", I renamed "fixing" to "arbitrary".
authorurbanc
Thu Oct 12 22:03:33 2006 +0200 (2006-10-12)
changeset 20998714a08286899
parent 20997 4b500d78cb4f
child 20999 9131d8e96dba
To be consistent with "induct", I renamed "fixing" to "arbitrary".
However I am not very fond of "arbitrary" - e.g. it clashes with
"arbitrary" of HOL. Both Gentzen (at least in the Szabo translation)
and Velleman (in How to prove it: a structured approach) use
"arbitrary".

Still, I wonder whether "generalising" is a good compromise?
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Oct 12 15:50:43 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Oct 12 22:03:33 2006 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4  local
     1.5  
     1.6  val avoidingN = "avoiding";
     1.7 -val fixingN = "fixing";
     1.8 +val fixingN = "arbitrary";  (* to be consistent with induct; hopefully this changes again *)
     1.9  val ruleN = "rule";
    1.10  
    1.11  val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;