src/HOL/IsaMakefile

   HOL-Number_Theory \
   HOL-Old_Number_Theory \
   HOL-Quotient_Examples \
   HOL-Predicate_Compile_Examples \
   HOL-Prolog \
+  HOL-Proofs-ex \
   HOL-Proofs-Extraction \
   HOL-Proofs-Lambda \
   HOL-SET_Protocol \
   HOL-Word-SMT_Examples \
   HOL-Statespace \

 HOL-Base: Pure $(OUT)/HOL-Base
 
 HOL-Plain: Pure $(OUT)/HOL-Plain
 
 HOL-Main: Pure $(OUT)/HOL-Main
-
-HOL-Proofs: Pure $(OUT)/HOL-Proofs
 
 Pure:
 	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
 
 $(OUT)/Pure: Pure

   Tools/simpdata.ML
 
 $(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
 	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
 
-PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
+PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
   Complete_Lattice.thy \
   Datatype.thy \
   Extraction.thy \
   Fields.thy \
   Finite_Set.thy \

   Tools/TFL/utils.ML
 
 $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
 	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
 
-$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
-	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
-
 HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
   Archimedean_Field.thy \
   Complex.thy \
   Complex_Main.thy \
   Deriv.thy \

   Tools/float_syntax.ML \
   Tools/SMT/smt_real.ML
 
 $(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
 	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
-
 
 
 ## HOL-Library
 
 HOL-Library: HOL $(OUT)/HOL-Library

 HOL-Unix: HOL $(LOG)/HOL-Unix.gz
 
 $(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy		\
   Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy			\
   Unix/document/root.bib Unix/document/root.tex
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
+	@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
 
 
 ## HOL-ZF
 
 HOL-ZF: HOL $(LOG)/HOL-ZF.gz

 $(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML		\
   Docs/document/root.tex
 	@$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs
 
 
+## HOL-Proofs
+
+HOL-Proofs: Pure $(OUT)/HOL-Proofs
+
+$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
+	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
+
+
+## HOL-Proofs-ex
+
+HOL-Proofs-ex: HOL-Proofs $(LOG)/HOL-Proofs-ex.gz
+
+$(LOG)/HOL-Proofs-ex.gz: $(OUT)/HOL-Proofs			\
+  Proofs/ex/ROOT.ML Proofs/ex/Hilbert_Classical.thy
+	@cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs ex
+
+
+## HOL-Proofs-Extraction
+
+HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
+
+$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs		\
+  Library/Efficient_Nat.thy Proofs/Extraction/Euclid.thy	\
+  Proofs/Extraction/Greatest_Common_Divisor.thy			\
+  Proofs/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.thy	\
+  Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML	\
+  Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy	\
+  Proofs/Extraction/document/root.tex				\
+  Proofs/Extraction/document/root.bib
+	@cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
+
+
 ## HOL-Proofs-Lambda
 
 HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
 
-$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs Lambda/Commutation.thy	\
-  Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy		\
-  Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy	\
-  Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy	\
-  Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy		\
-  Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex
-	@$(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
+$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs				\
+  Proofs/Lambda/Commutation.thy Proofs/Lambda/Eta.thy			\
+  Proofs/Lambda/InductTermi.thy Proofs/Lambda/Lambda.thy		\
+  Proofs/Lambda/ListApplication.thy Proofs/Lambda/ListBeta.thy		\
+  Proofs/Lambda/ListOrder.thy Proofs/Lambda/NormalForm.thy		\
+  Proofs/Lambda/ParRed.thy Proofs/Lambda/Standardization.thy		\
+  Proofs/Lambda/StrongNorm.thy Proofs/Lambda/Type.thy			\
+  Proofs/Lambda/WeakNorm.thy Proofs/Lambda/ROOT.ML			\
+  Proofs/Lambda/document/root.bib Proofs/Lambda/document/root.tex
+	@cd Proofs; $(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
 
 
 ## HOL-Prolog
 
 HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz

   Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy			\
   Bali/document/root.tex
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
 
 
-## HOL-Proofs-Extraction
-
-HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
-
-$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs			\
-  Library/Efficient_Nat.thy Extraction/Euclid.thy			\
-  Extraction/Greatest_Common_Divisor.thy Extraction/Higman.thy		\
-  Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML	\
-  Extraction/Util.thy Extraction/Warshall.thy				\
-  Extraction/document/root.tex Extraction/document/root.bib
-	@$(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
-
-
 ## HOL-IOA
 
 HOL-IOA: HOL $(LOG)/HOL-IOA.gz
 
 $(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML	\

 ## HOL-ex
 
 HOL-ex: HOL $(LOG)/HOL-ex.gz
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy	\
-  Number_Theory/Primes.thy						\
-  ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy		\
-  ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy		\
-  ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
-  ex/CodegenSML_Test.thy ex/Coherent.thy ex/Dedekind_Real.thy		\
-  ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy	\
-  ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy	\
-  ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy		\
-  ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy			\
+  Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
+  ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy	\
+  ex/BinEx.thy ex/Binary.thy ex/CTL.thy ex/Chinese.thy			\
+  ex/Classical.thy ex/CodegenSML_Test.thy ex/Coherent.thy		\
+  ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy			\
+  ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy		\
+  ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
+  ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
   ex/Induction_Schema.thy ex/InductiveInvariant.thy			\
   ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
-  ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy				\
-  ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
-  ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
-  ex/PresburgerEx.thy ex/Primrec.thy 					\
-  ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy 	\
+  ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy		\
+  ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
+  ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
+  ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy		\
   ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
   ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\
   ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy	\
-  ex/Unification.thy ex/While_Combinator_Example.thy ex/document/root.bib \
-	ex/document/root.tex		\
-  ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
+  ex/Unification.thy ex/While_Combinator_Example.thy			\
+  ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML	\
+  ex/svc_test.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
 
 
 ## HOL-Isar_Examples
 

   Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy		\
   Probability/Lebesgue_Measure.thy \
   Library/Nat_Bijection.thy Library/Countable.thy
 	@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability
 
+
 ## HOL-Nominal
 
 HOL-Nominal: HOL $(OUT)/HOL-Nominal
 
 $(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \

 
 ## HOL-Nominal-Examples
 
 HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
 
-$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
+$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
   Nominal/Examples/Nominal_Examples.thy \
   Nominal/Examples/CK_Machine.thy \
   Nominal/Examples/CR.thy \
   Nominal/Examples/CR_Takahashi.thy \
   Nominal/Examples/Class1.thy \

 		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz	\
 		$(LOG)/HOL-Number_Theory.gz				\
 		$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz	\
 		$(LOG)/HOL-Predicate_Compile_Examples.gz		\
 		$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz		\
-		$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-Extraction.gz	\
+		$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz		\
+		$(LOG)/HOL-Proofs-Extraction.gz				\
 		$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz	\
 		$(LOG)/HOL-Word-SMT_Examples.gz				\
 		$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz		\
 		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
 		$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz		\