HOL-Lambda: usedir -m no_brackets;
authorwenzelm
Fri, 19 Jan 2007 22:08:07 +0100
changeset 2210033d7468302bb
parent 22099 5dc00ac4bd8e
child 22101 6d13239d5f52
HOL-Lambda: usedir -m no_brackets;
src/HOL/IsaMakefile
src/HOL/Lambda/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 19 22:08:06 2007 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 19 22:08:07 2007 +0100
     1.3 @@ -482,7 +482,7 @@
     1.4    Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \
     1.5    Lambda/WeakNorm.thy Lambda/ROOT.ML \
     1.6    Lambda/document/root.bib Lambda/document/root.tex
     1.7 -	@$(ISATOOL) usedir -g true $(OUT)/HOL Lambda
     1.8 +	@$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
     1.9  
    1.10  
    1.11  ## HOL-Prolog
     2.1 --- a/src/HOL/Lambda/ROOT.ML	Fri Jan 19 22:08:06 2007 +0100
     2.2 +++ b/src/HOL/Lambda/ROOT.ML	Fri Jan 19 22:08:07 2007 +0100
     2.3 @@ -6,7 +6,6 @@
     2.4  
     2.5  Syntax.ambiguity_level := 100;
     2.6  proofs := 2;
     2.7 -IsarOutput.modes := "no_brackets" :: !IsarOutput.modes;
     2.8  
     2.9  use_thy "Eta";
    2.10  no_document use_thy "Accessible_Part";