# HG changeset patch
# User oheimb
# Date 982249235 -3600
# Node ID 7c66f3dc7d1473f13254d76a3dad1e7634067f1a
# Parent  09622301ca078d3d7ad05d4195b1deacf8ad55e6
Ord.thy/.ML converted to Isar

diff -r 09622301ca07 -r 7c66f3dc7d14 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Feb 15 15:56:51 2001 +0100
+++ b/src/HOL/IsaMakefile	Thu Feb 15 16:00:35 2001 +0100
@@ -86,7 +86,7 @@
   Inverse_Image.ML Inverse_Image.thy Lfp.ML \
   Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
   Nat.thy NatArith.ML NatArith.thy NatDef.ML NatDef.thy Numeral.thy \
-  Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy \
+  Option.ML Option.thy Ord.thy Power.ML Power.thy PreList.thy \
   Product_Type_lemmas.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
   Relation.ML Relation.thy Relation_Power.ML Relation_Power.thy \
   SVC_Oracle.ML SVC_Oracle.thy Set.ML Set.thy SetInterval.ML \