# HG changeset patch
# User wenzelm
# Date 1126728275 -7200
# Node ID c01de5939f5b123ea06c00507f7afc6d08b8558e
# Parent  3eb21fb8c2ec42ad7b359a252a55035ea6d0c94d
tuned;

diff -r 3eb21fb8c2ec -r c01de5939f5b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Sep 14 22:04:34 2005 +0200
+++ b/src/HOL/IsaMakefile	Wed Sep 14 22:04:35 2005 +0200
@@ -78,27 +78,27 @@
   $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML		\
   $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
   $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
-  Binomial.thy Commutative_Ring.thy Datatype.ML Datatype.thy \
-  Datatype_Universe.thy Divides.thy \
+  Binomial.thy Commutative_Ring.thy Datatype.ML Datatype.thy			\
+  Datatype_Universe.thy Divides.thy						\
   Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
-  FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy		\
+  FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy	\
   Infinite_Set.thy Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy		\
   Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy			\
   Integ/Parity.thy Integ/Presburger.thy Integ/cooper_dec.ML			\
-  Integ/cooper_proof.ML Integ/reflected_presburger.ML \
+  Integ/cooper_proof.ML Integ/reflected_presburger.ML				\
   Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
   Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
-  Lattice_Locales.thy List.ML List.thy Main.ML Main.thy Map.thy		\
+  Lattice_Locales.thy List.ML List.thy Main.ML Main.thy Map.thy			\
   Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy			\
   Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
   ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
   Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
   Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML		\
-  Tools/ATP/VampCommunication.ML			\
+  Tools/ATP/VampCommunication.ML						\
   Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
   Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML			\
   Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
-  Tools/ATP/watcher.ML 	Tools/comm_ring.ML				\
+  Tools/ATP/watcher.ML 	Tools/comm_ring.ML					\
   Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
   Tools/datatype_codegen.ML Tools/datatype_package.ML				\
   Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
@@ -585,21 +585,21 @@
 
 HOL-ex: HOL $(LOG)/HOL-ex.gz
 
-$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy \
-  ex/BT.thy ex/BinEx.thy ex/Commutative_RingEx.thy \
-  ex/Commutative_Ring_Complete.thy ex/Higher_Order_Logic.thy \
-  ex/Hilbert_Classical.thy ex/InSort.thy \
-  ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy\
-  ex/Intuitionistic.thy \
-  ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy \
-  ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
-  ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Reflected_Presburger.thy \
-  ex/Primrec.thy ex/Puzzle.thy \
-  ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
-  ex/Refute_Examples.thy \
-  ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
-  ex/Tarski.thy ex/Tuple.thy ex/Classical.thy \
-  ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML \
+$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy						\
+  ex/BT.thy ex/BinEx.thy ex/Commutative_RingEx.thy					\
+  ex/Commutative_Ring_Complete.thy ex/Higher_Order_Logic.thy				\
+  ex/Hilbert_Classical.thy ex/InSort.thy						\
+  ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy				\
+  ex/Intuitionistic.thy									\
+  ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy					\
+  ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy				\
+  ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Reflected_Presburger.thy		\
+  ex/Primrec.thy ex/Puzzle.thy								\
+  ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy	\
+  ex/Refute_Examples.thy								\
+  ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy					\
+  ex/Tarski.thy ex/Tuple.thy ex/Classical.thy						\
+  ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML				\
   ex/svc_test.ML ex/svc_test.thy ex/document/root.bib ex/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/HOL ex
 
diff -r 3eb21fb8c2ec -r c01de5939f5b src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed Sep 14 22:04:34 2005 +0200
+++ b/src/Pure/Isar/calculation.ML	Wed Sep 14 22:04:35 2005 +0200
@@ -153,10 +153,7 @@
 
 fun print_calculation false _ _ = ()
   | print_calculation true ctxt calc =
-      Pretty.writeln (Pretty.big_list "calculation:" (map (ProofContext.pretty_thm ctxt) calc));
-(* FIXME 
       Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
-*)
 
 
 (* also and finally *)
diff -r 3eb21fb8c2ec -r c01de5939f5b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Sep 14 22:04:34 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Sep 14 22:04:35 2005 +0200
@@ -2105,7 +2105,7 @@
 val theorem_in_locale_i =
   gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement;
 
-fun smart_theorem kind NONE a [] concl =   (* FIXME tune *)
+fun smart_theorem kind NONE a [] concl =
       Proof.theorem kind (K (K I)) NONE a concl o ProofContext.init
   | smart_theorem kind NONE a elems concl =
       theorem kind (K (K I)) a elems concl
diff -r 3eb21fb8c2ec -r c01de5939f5b src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Sep 14 22:04:34 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Sep 14 22:04:35 2005 +0200
@@ -1401,7 +1401,7 @@
 
     (*theory*)
     val pretty_thy = Pretty.block
-      [Pretty.str "Theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)];  (* FIXME lowercase *)
+      [Pretty.str "theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)];
 
     (*defaults*)
     fun prt_atom prt prtT (x, X) = Pretty.block