author | urbanc |

Thu Oct 12 22:03:33 2006 +0200 (2006-10-12) | |

changeset 20998 | 714a08286899 |

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?

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?

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;