tuned;
authorwenzelm
Wed Sep 14 22:04:35 2005 +0200 (2005-09-14)
changeset 17384c01de5939f5b
parent 17383 3eb21fb8c2ec
child 17385 4dcae6e62268
tuned;
src/HOL/IsaMakefile
src/Pure/Isar/calculation.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Sep 14 22:04:34 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Sep 14 22:04:35 2005 +0200
     1.3 @@ -78,27 +78,27 @@
     1.4    $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML		\
     1.5    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
     1.6    $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
     1.7 -  Binomial.thy Commutative_Ring.thy Datatype.ML Datatype.thy \
     1.8 -  Datatype_Universe.thy Divides.thy \
     1.9 +  Binomial.thy Commutative_Ring.thy Datatype.ML Datatype.thy			\
    1.10 +  Datatype_Universe.thy Divides.thy						\
    1.11    Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
    1.12 -  FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy		\
    1.13 +  FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy	\
    1.14    Infinite_Set.thy Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy		\
    1.15    Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy			\
    1.16    Integ/Parity.thy Integ/Presburger.thy Integ/cooper_dec.ML			\
    1.17 -  Integ/cooper_proof.ML Integ/reflected_presburger.ML \
    1.18 +  Integ/cooper_proof.ML Integ/reflected_presburger.ML				\
    1.19    Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
    1.20    Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
    1.21 -  Lattice_Locales.thy List.ML List.thy Main.ML Main.thy Map.thy		\
    1.22 +  Lattice_Locales.thy List.ML List.thy Main.ML Main.thy Map.thy			\
    1.23    Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy			\
    1.24    Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
    1.25    ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
    1.26    Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
    1.27    Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML		\
    1.28 -  Tools/ATP/VampCommunication.ML			\
    1.29 +  Tools/ATP/VampCommunication.ML						\
    1.30    Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
    1.31    Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML			\
    1.32    Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
    1.33 -  Tools/ATP/watcher.ML 	Tools/comm_ring.ML				\
    1.34 +  Tools/ATP/watcher.ML 	Tools/comm_ring.ML					\
    1.35    Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
    1.36    Tools/datatype_codegen.ML Tools/datatype_package.ML				\
    1.37    Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
    1.38 @@ -585,21 +585,21 @@
    1.39  
    1.40  HOL-ex: HOL $(LOG)/HOL-ex.gz
    1.41  
    1.42 -$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy \
    1.43 -  ex/BT.thy ex/BinEx.thy ex/Commutative_RingEx.thy \
    1.44 -  ex/Commutative_Ring_Complete.thy ex/Higher_Order_Logic.thy \
    1.45 -  ex/Hilbert_Classical.thy ex/InSort.thy \
    1.46 -  ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy\
    1.47 -  ex/Intuitionistic.thy \
    1.48 -  ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy \
    1.49 -  ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
    1.50 -  ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Reflected_Presburger.thy \
    1.51 -  ex/Primrec.thy ex/Puzzle.thy \
    1.52 -  ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
    1.53 -  ex/Refute_Examples.thy \
    1.54 -  ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
    1.55 -  ex/Tarski.thy ex/Tuple.thy ex/Classical.thy \
    1.56 -  ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML \
    1.57 +$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy						\
    1.58 +  ex/BT.thy ex/BinEx.thy ex/Commutative_RingEx.thy					\
    1.59 +  ex/Commutative_Ring_Complete.thy ex/Higher_Order_Logic.thy				\
    1.60 +  ex/Hilbert_Classical.thy ex/InSort.thy						\
    1.61 +  ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy				\
    1.62 +  ex/Intuitionistic.thy									\
    1.63 +  ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy					\
    1.64 +  ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy				\
    1.65 +  ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Reflected_Presburger.thy		\
    1.66 +  ex/Primrec.thy ex/Puzzle.thy								\
    1.67 +  ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy	\
    1.68 +  ex/Refute_Examples.thy								\
    1.69 +  ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy					\
    1.70 +  ex/Tarski.thy ex/Tuple.thy ex/Classical.thy						\
    1.71 +  ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML				\
    1.72    ex/svc_test.ML ex/svc_test.thy ex/document/root.bib ex/document/root.tex
    1.73  	@$(ISATOOL) usedir $(OUT)/HOL ex
    1.74  
     2.1 --- a/src/Pure/Isar/calculation.ML	Wed Sep 14 22:04:34 2005 +0200
     2.2 +++ b/src/Pure/Isar/calculation.ML	Wed Sep 14 22:04:35 2005 +0200
     2.3 @@ -153,10 +153,7 @@
     2.4  
     2.5  fun print_calculation false _ _ = ()
     2.6    | print_calculation true ctxt calc =
     2.7 -      Pretty.writeln (Pretty.big_list "calculation:" (map (ProofContext.pretty_thm ctxt) calc));
     2.8 -(* FIXME 
     2.9        Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
    2.10 -*)
    2.11  
    2.12  
    2.13  (* also and finally *)
     3.1 --- a/src/Pure/Isar/locale.ML	Wed Sep 14 22:04:34 2005 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Wed Sep 14 22:04:35 2005 +0200
     3.3 @@ -2105,7 +2105,7 @@
     3.4  val theorem_in_locale_i =
     3.5    gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement;
     3.6  
     3.7 -fun smart_theorem kind NONE a [] concl =   (* FIXME tune *)
     3.8 +fun smart_theorem kind NONE a [] concl =
     3.9        Proof.theorem kind (K (K I)) NONE a concl o ProofContext.init
    3.10    | smart_theorem kind NONE a elems concl =
    3.11        theorem kind (K (K I)) a elems concl
     4.1 --- a/src/Pure/Isar/proof_context.ML	Wed Sep 14 22:04:34 2005 +0200
     4.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Sep 14 22:04:35 2005 +0200
     4.3 @@ -1401,7 +1401,7 @@
     4.4  
     4.5      (*theory*)
     4.6      val pretty_thy = Pretty.block
     4.7 -      [Pretty.str "Theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)];  (* FIXME lowercase *)
     4.8 +      [Pretty.str "theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)];
     4.9  
    4.10      (*defaults*)
    4.11      fun prt_atom prt prtT (x, X) = Pretty.block