src/HOL/Real/ex/ROOT.ML
author wenzelm
Wed, 06 Mar 2002 17:48:08 +0100
changeset 13030 5765aa72afac
parent 12077 d46a32262bac
permissions -rw-r--r--
moved to Hyperreal-ex;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7577
644f9b4ae764 proper theory setup for Real/ex/BinEx;
wenzelm
parents: 7393
diff changeset
     1
(*  Title:      HOL/Real/ex/ROOT.ML
7392
4137c951b36b new directory HOL/Real/ex of real examples
paulson
parents:
diff changeset
     2
    ID:         $Id$
4137c951b36b new directory HOL/Real/ex of real examples
paulson
parents:
diff changeset
     3
11598
4f26832a7b86 updated;
wenzelm
parents: 9000
diff changeset
     4
Miscellaneous HOL-Real Examples.
7392
4137c951b36b new directory HOL/Real/ex of real examples
paulson
parents:
diff changeset
     5
*)
4137c951b36b new directory HOL/Real/ex of real examples
paulson
parents:
diff changeset
     6
7577
644f9b4ae764 proper theory setup for Real/ex/BinEx;
wenzelm
parents: 7393
diff changeset
     7
time_use_thy "BinEx";