--- 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
--- 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 *)
--- 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
--- 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