# HG changeset patch # User haftmann # Date 1233137022 -3600 # Node ID ac31940cfb69b84298e34a4ab8c50d191a383de4 # Parent 24e73987bfe2b83f4b6ede6691caad69c7009ff6 Plain, Main form meeting points in import hierarchy diff -r 24e73987bfe2 -r ac31940cfb69 src/HOL/Dense_Linear_Order.thy --- a/src/HOL/Dense_Linear_Order.thy Wed Jan 28 11:03:16 2009 +0100 +++ b/src/HOL/Dense_Linear_Order.thy Wed Jan 28 11:03:42 2009 +0100 @@ -1,10 +1,12 @@ -(* Author: Amine Chaieb, TU Muenchen *) +(* Title : HOL/Dense_Linear_Order.thy + Author : Amine Chaieb, TU Muenchen +*) header {* Dense linear order without endpoints and a quantifier elimination procedure in Ferrante and Rackoff style *} theory Dense_Linear_Order -imports Plain Groebner_Basis +imports Plain Groebner_Basis Main uses "~~/src/HOL/Tools/Qelim/langford_data.ML" "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML" diff -r 24e73987bfe2 -r ac31940cfb69 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Wed Jan 28 11:03:16 2009 +0100 +++ b/src/HOL/Equiv_Relations.thy Wed Jan 28 11:03:42 2009 +0100 @@ -1,12 +1,11 @@ -(* ID: $Id$ - Authors: Lawrence C Paulson, Cambridge University Computer Laboratory +(* Authors: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge *) header {* Equivalence Relations in Higher-Order Set Theory *} theory Equiv_Relations -imports Finite_Set Relation +imports Finite_Set Relation Plain begin subsection {* Equivalence relations *} diff -r 24e73987bfe2 -r ac31940cfb69 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Jan 28 11:03:16 2009 +0100 +++ b/src/HOL/GCD.thy Wed Jan 28 11:03:42 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/GCD.thy - ID: $Id$ Author: Christophe Tabacznyj and Lawrence C Paulson Copyright 1996 University of Cambridge *) @@ -7,7 +6,7 @@ header {* The Greatest Common Divisor *} theory GCD -imports Plain Presburger +imports Plain Presburger Main begin text {* diff -r 24e73987bfe2 -r ac31940cfb69 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Wed Jan 28 11:03:16 2009 +0100 +++ b/src/HOL/Hilbert_Choice.thy Wed Jan 28 11:03:42 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Hilbert_Choice.thy - ID: $Id$ Author: Lawrence C Paulson Copyright 2001 University of Cambridge *) @@ -7,7 +6,7 @@ header {* Hilbert's Epsilon-Operator and the Axiom of Choice *} theory Hilbert_Choice -imports Nat Wellfounded +imports Nat Wellfounded Plain uses ("Tools/meson.ML") ("Tools/specification_package.ML") begin