# HG changeset patch # User bulwahn # Date 1294412350 -3600 # Node ID 52d39af5e6809fa9ad282917e87fcfa83b5716a4 # Parent ea56b98aee83f14acb8f427bd159d96d0de54aec# Parent f0db8f40d6568501d76952d67d8c1fd77d6d40d7 merged diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/CTL.thy --- a/src/HOL/ex/CTL.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/CTL.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/CTL.thy - ID: $Id$ Author: Gertrud Bauer *) diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/Guess.thy --- a/src/HOL/ex/Guess.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/Guess.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* - ID: $Id$ Author: Makarius *) diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/Hex_Bin_Examples.thy --- a/src/HOL/ex/Hex_Bin_Examples.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/Hex_Bin_Examples.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/Hex_Bin_Examples.thy - ID: $Id$ Author: Gerwin Klein, NICTA *) diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/Higher_Order_Logic.thy --- a/src/HOL/ex/Higher_Order_Logic.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/Higher_Order_Logic.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/Higher_Order_Logic.thy - ID: $Id$ Author: Gertrud Bauer and Markus Wenzel, TU Muenchen *) diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/Intuitionistic.thy --- a/src/HOL/ex/Intuitionistic.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/Intuitionistic.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/Intuitionistic.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/MT.thy --- a/src/HOL/ex/MT.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/MT.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/MT.thy - ID: $Id$ Author: Jacob Frost, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/MonoidGroup.thy --- a/src/HOL/ex/MonoidGroup.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/MonoidGroup.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/MonoidGroup.thy - ID: $Id$ Author: Markus Wenzel *) diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/Primrec.thy --- a/src/HOL/ex/Primrec.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/Primrec.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/Primrec.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/SVC_Oracle.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/SVC_Oracle.thy - ID: $Id$ Author: Lawrence C Paulson Copyright 1999 University of Cambridge diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/Sorting.thy --- a/src/HOL/ex/Sorting.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/Sorting.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/sorting.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1994 TU Muenchen *) diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/Unification.thy --- a/src/HOL/ex/Unification.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/Unification.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,4 +1,4 @@ -(* ID: $Id$ +(* Author: Alexander Krauss, Technische Universitaet Muenchen *) diff -r f0db8f40d656 -r 52d39af5e680 src/HOL/ex/set.thy --- a/src/HOL/ex/set.thy Fri Jan 07 15:39:13 2011 +0100 +++ b/src/HOL/ex/set.thy Fri Jan 07 15:59:10 2011 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/set.thy - ID: $Id$ Author: Tobias Nipkow and Lawrence C Paulson Copyright 1991 University of Cambridge *)