hardcoded nbe and sml into value command
authorhaftmann
Fri May 09 08:13:37 2014 +0200 (2014-05-09)
changeset 569274044a7d1720f
parent 56926 aaea99edc040
child 56928 1e50fddbe1f5
hardcoded nbe and sml into value command
NEWS
src/Doc/Codegen/Evaluation.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/HOL/Code_Evaluation.thy
src/HOL/IMP/Abs_Int1_parity.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
src/HOL/Tools/value.ML
src/HOL/ex/Eval_Examples.thy
src/HOL/ex/Normalization_by_Evaluation.thy
src/HOL/ex/Parallel_Example.thy
     1.1 --- a/NEWS	Fri May 09 08:13:36 2014 +0200
     1.2 +++ b/NEWS	Fri May 09 08:13:37 2014 +0200
     1.3 @@ -204,8 +204,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Command and antiquotation ''value'' are hardcoded against nbe and
     1.8 +ML now.  Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Separate command ''approximate'' for approximative computation
    1.11 -in Decision_Procs/Approximation.  Minor INCOMPATBILITY.
    1.12 +in Decision_Procs/Approximation.  Minor INCOMPATIBILITY.
    1.13  
    1.14  * Adjustion of INF and SUP operations:
    1.15    * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
     2.1 --- a/src/Doc/Codegen/Evaluation.thy	Fri May 09 08:13:36 2014 +0200
     2.2 +++ b/src/Doc/Codegen/Evaluation.thy	Fri May 09 08:13:37 2014 +0200
     2.3 @@ -90,18 +90,12 @@
     2.4  value %quote "42 / (12 :: rat)"
     2.5  
     2.6  text {*
     2.7 -  \noindent By default @{command value} tries all available evaluation
     2.8 -  techniques and prints the result of the first succeeding one.  A particular
     2.9 -  technique may be specified in square brackets, e.g.
    2.10 -*}
    2.11 +  \noindent @{command value} tries first to evaluate using ML, falling
    2.12 +  back to normalization by evaluation if this fails.
    2.13  
    2.14 -value %quote [nbe] "42 / (12 :: rat)"
    2.15 -
    2.16 -text {*
    2.17    To employ dynamic evaluation in the document generation, there is also
    2.18 -  a @{text value} antiquotation. By default, it also tries all available evaluation
    2.19 -  techniques and prints the result of the first succeeding one, unless a particular
    2.20 -  technique is specified in square brackets.
    2.21 +  a @{text value} antiquotation with the same evaluation techniques 
    2.22 +  as @{command value}.
    2.23  
    2.24    Static evaluation freezes the code generator configuration at a
    2.25    certain point and uses this context whenever evaluation is issued
    2.26 @@ -172,10 +166,7 @@
    2.27    \fontsize{9pt}{12pt}\selectfont
    2.28    \begin{tabular}{ll||c|c|c}
    2.29      & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
    2.30 -    \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
    2.31 -      & interactive evaluation 
    2.32 -      & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
    2.33 -      \tabularnewline
    2.34 +    \multirow{4}{1ex}{\rotatebox{90}{dynamic}}
    2.35      & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
    2.36      & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
    2.37      & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
     3.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri May 09 08:13:36 2014 +0200
     3.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri May 09 08:13:37 2014 +0200
     3.3 @@ -2114,7 +2114,7 @@
     3.4    \end{matharray}
     3.5  
     3.6    @{rail \<open>
     3.7 -    @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
     3.8 +    @@{command (HOL) value} modes? @{syntax term}
     3.9      ;
    3.10  
    3.11      @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
    3.12 @@ -2144,13 +2144,8 @@
    3.13    \item @{command (HOL) "value"}~@{text t} evaluates and prints a
    3.14    term; optionally @{text modes} can be specified, which are appended
    3.15    to the current print mode; see \secref{sec:print-modes}.
    3.16 -  Internally, the evaluation is performed by registered evaluators,
    3.17 -  which are invoked sequentially until a result is returned.
    3.18 -  Alternatively a specific evaluator can be selected using square
    3.19 -  brackets; typical evaluators use the current set of code equations
    3.20 -  to normalize and include @{text simp} for fully symbolic evaluation
    3.21 -  using the simplifier, @{text nbe} for \emph{normalization by
    3.22 -  evaluation} and \emph{code} for code generation in SML.
    3.23 +  Evaluation is tried first using ML, falling
    3.24 +  back to normalization by evaluation if this fails.
    3.25  
    3.26    \item @{command (HOL) "values"}~@{text t} enumerates a set
    3.27    comprehension by evaluation and prints its values up to the given
     4.1 --- a/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:36 2014 +0200
     4.2 +++ b/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:37 2014 +0200
     4.3 @@ -158,11 +158,6 @@
     4.4  
     4.5  ML_file "~~/src/HOL/Tools/value.ML"
     4.6  
     4.7 -setup {*
     4.8 -  Value.add_evaluator ("nbe", Nbe.dynamic_value)
     4.9 -  #> Value.add_evaluator ("code", Code_Evaluation.dynamic_value_strict)
    4.10 -*}
    4.11 -
    4.12  
    4.13  subsection {* Generic reification *}
    4.14  
     5.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Fri May 09 08:13:36 2014 +0200
     5.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri May 09 08:13:37 2014 +0200
     5.3 @@ -134,7 +134,7 @@
     5.4  definition "test1_parity =
     5.5    ''x'' ::= N 1;;
     5.6    WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
     5.7 -value [code] "show_acom (the(AI_parity test1_parity))"
     5.8 +value "show_acom (the(AI_parity test1_parity))"
     5.9  
    5.10  definition "test2_parity =
    5.11    ''x'' ::= N 1;;
     6.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Fri May 09 08:13:36 2014 +0200
     6.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Fri May 09 08:13:37 2014 +0200
     6.3 @@ -100,12 +100,12 @@
     6.4    WHILE Less (V ''x'') (N 1)
     6.5    DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'';; ''z'' ::= V ''u'')"
     6.6  
     6.7 -value [code] "list (AI_const test1_const Top)"
     6.8 -value [code] "list (AI_const test2_const Top)"
     6.9 -value [code] "list (AI_const test3_const Top)"
    6.10 -value [code] "list (AI_const test4_const Top)"
    6.11 -value [code] "list (AI_const test5_const Top)"
    6.12 -value [code] "list (AI_const test6_const Top)"
    6.13 -value [code] "list (AI_const test7_const Top)"
    6.14 +value "list (AI_const test1_const Top)"
    6.15 +value "list (AI_const test2_const Top)"
    6.16 +value "list (AI_const test3_const Top)"
    6.17 +value "list (AI_const test4_const Top)"
    6.18 +value "list (AI_const test5_const Top)"
    6.19 +value "list (AI_const test6_const Top)"
    6.20 +value "list (AI_const test7_const Top)"
    6.21  
    6.22  end
     7.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Fri May 09 08:13:36 2014 +0200
     7.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Fri May 09 08:13:37 2014 +0200
     7.3 @@ -213,22 +213,22 @@
     7.4  "list_up bot = bot" |
     7.5  "list_up (Up x) = Up(list x)"
     7.6  
     7.7 -value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
     7.8 -value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
     7.9 -value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
    7.10 +value "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
    7.11 +value "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
    7.12 +value "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
    7.13   (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
    7.14 -value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
    7.15 +value "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
    7.16   (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
    7.17 -value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
    7.18 +value "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
    7.19    (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
    7.20 -value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
    7.21 +value "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
    7.22    (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
    7.23  
    7.24 -value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
    7.25 +value "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
    7.26    (Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
    7.27 -value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
    7.28 +value "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
    7.29    (Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
    7.30 -value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
    7.31 +value "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
    7.32    (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
    7.33  
    7.34  definition "test_ivl1 =
    7.35 @@ -236,7 +236,7 @@
    7.36   IF Less (V ''x'') (V ''y'')
    7.37   THEN ''y'' ::= Plus (V ''y'') (V ''x'')
    7.38   ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
    7.39 -value [code] "list_up(AI_ivl test_ivl1 Top)"
    7.40 +value "list_up(AI_ivl test_ivl1 Top)"
    7.41  
    7.42  value "list_up (AI_ivl test3_const Top)"
    7.43  
    7.44 @@ -247,24 +247,24 @@
    7.45  definition "test2_ivl =
    7.46   ''y'' ::= N 7;;
    7.47   WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
    7.48 -value [code] "list_up(AI_ivl test2_ivl Top)"
    7.49 +value "list_up(AI_ivl test2_ivl Top)"
    7.50  
    7.51  definition "test3_ivl =
    7.52   ''x'' ::= N 0;; ''y'' ::= N 100;; ''z'' ::= Plus (V ''x'') (V ''y'');;
    7.53   WHILE Less (V ''x'') (N 11)
    7.54   DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N -1))"
    7.55 -value [code] "list_up(AI_ivl test3_ivl Top)"
    7.56 +value "list_up(AI_ivl test3_ivl Top)"
    7.57  
    7.58  definition "test4_ivl =
    7.59   ''x'' ::= N 0;; ''y'' ::= N 0;;
    7.60   WHILE Less (V ''x'') (N 1001)
    7.61   DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
    7.62 -value [code] "list_up(AI_ivl test4_ivl Top)"
    7.63 +value "list_up(AI_ivl test4_ivl Top)"
    7.64  
    7.65  text{* Nontermination not detected: *}
    7.66  definition "test5_ivl =
    7.67   ''x'' ::= N 0;;
    7.68   WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
    7.69 -value [code] "list_up(AI_ivl test5_ivl Top)"
    7.70 +value "list_up(AI_ivl test5_ivl Top)"
    7.71  
    7.72  end
     8.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Fri May 09 08:13:36 2014 +0200
     8.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Fri May 09 08:13:37 2014 +0200
     8.3 @@ -200,8 +200,8 @@
     8.4  and aval_ivl' = aval'
     8.5  proof qed (auto simp: iter'_pfp_above)
     8.6  
     8.7 -value [code] "list_up(AI_ivl' test3_ivl Top)"
     8.8 -value [code] "list_up(AI_ivl' test4_ivl Top)"
     8.9 -value [code] "list_up(AI_ivl' test5_ivl Top)"
    8.10 +value "list_up(AI_ivl' test3_ivl Top)"
    8.11 +value "list_up(AI_ivl' test4_ivl Top)"
    8.12 +value "list_up(AI_ivl' test5_ivl Top)"
    8.13  
    8.14  end
     9.1 --- a/src/HOL/Library/Extended_Real.thy	Fri May 09 08:13:36 2014 +0200
     9.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri May 09 08:13:37 2014 +0200
     9.3 @@ -2444,10 +2444,10 @@
     9.4  
     9.5  (* A small list of simple arithmetic expressions *)
     9.6  
     9.7 -value [code] "- \<infinity> :: ereal"
     9.8 -value [code] "\<bar>-\<infinity>\<bar> :: ereal"
     9.9 -value [code] "4 + 5 / 4 - ereal 2 :: ereal"
    9.10 -value [code] "ereal 3 < \<infinity>"
    9.11 -value [code] "real (\<infinity>::ereal) = 0"
    9.12 +value "- \<infinity> :: ereal"
    9.13 +value "\<bar>-\<infinity>\<bar> :: ereal"
    9.14 +value "4 + 5 / 4 - ereal 2 :: ereal"
    9.15 +value "ereal 3 < \<infinity>"
    9.16 +value "real (\<infinity>::ereal) = 0"
    9.17  
    9.18  end
    10.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri May 09 08:13:36 2014 +0200
    10.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri May 09 08:13:37 2014 +0200
    10.3 @@ -452,8 +452,8 @@
    10.4  values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
    10.5  values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
    10.6  
    10.7 -value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
    10.8 -value [code] "Predicate.the (slice ([]::int list))"
    10.9 +value "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
   10.10 +value "Predicate.the (slice ([]::int list))"
   10.11  
   10.12  
   10.13  text {* tricky case with alternative rules *}
   10.14 @@ -830,7 +830,7 @@
   10.15  
   10.16  code_pred divmod_rel .
   10.17  thm divmod_rel.equation
   10.18 -value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
   10.19 +value "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
   10.20  
   10.21  subsection {* Transforming predicate logic into logic programs *}
   10.22  
    11.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri May 09 08:13:36 2014 +0200
    11.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri May 09 08:13:37 2014 +0200
    11.3 @@ -183,7 +183,7 @@
    11.4  quickcheck[tester = smart_exhaustive]
    11.5  oops
    11.6  
    11.7 -value [code] "prop_regex a_sol"
    11.8 +value "prop_regex a_sol"
    11.9  
   11.10  
   11.11  end
    12.1 --- a/src/HOL/Tools/value.ML	Fri May 09 08:13:36 2014 +0200
    12.2 +++ b/src/HOL/Tools/value.ML	Fri May 09 08:13:37 2014 +0200
    12.3 @@ -1,53 +1,30 @@
    12.4 -(*  Title:      Tools/value.ML
    12.5 +(*  Title:      HOL/Tools/value.ML
    12.6      Author:     Florian Haftmann, TU Muenchen
    12.7  
    12.8 -Generic value command for arbitrary evaluators.
    12.9 +Evaluation using nbe or SML.
   12.10  *)
   12.11  
   12.12  signature VALUE =
   12.13  sig
   12.14    val value: Proof.context -> term -> term
   12.15 -  val value_select: string -> Proof.context -> term -> term
   12.16 -  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
   12.17 -  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
   12.18 +  val value_cmd: string list -> string -> Toplevel.state -> unit
   12.19  end;
   12.20  
   12.21  structure Value : VALUE =
   12.22  struct
   12.23  
   12.24 -structure Evaluator = Theory_Data
   12.25 -(
   12.26 -  type T = (string * (Proof.context -> term -> term)) list;
   12.27 -  val empty = [];
   12.28 -  val extend = I;
   12.29 -  fun merge data : T = AList.merge (op =) (K true) data;
   12.30 -)
   12.31 -
   12.32 -val add_evaluator = Evaluator.map o AList.update (op =);
   12.33 -
   12.34 -fun value_select name ctxt =
   12.35 -  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
   12.36 -   of NONE => error ("No such evaluator: " ^ name)
   12.37 -    | SOME f => f ctxt;
   12.38 +fun value ctxt t =
   12.39 +  if null (Term.add_frees t [])
   12.40 +  then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
   12.41 +    SOME t' => t'
   12.42 +  | NONE => Nbe.dynamic_value ctxt t
   12.43 +  else Nbe.dynamic_value ctxt t;
   12.44  
   12.45 -fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
   12.46 -  in if null evaluators then error "No evaluators"
   12.47 -  else let val (evaluators, (_, evaluator)) = split_last evaluators
   12.48 -    in case get_first (fn (_, f) => try (f ctxt) t) evaluators
   12.49 -     of SOME t' => t'
   12.50 -      | NONE => evaluator ctxt t
   12.51 -  end end;
   12.52 -
   12.53 -fun value_maybe_select some_name =
   12.54 -  case some_name
   12.55 -    of NONE => value
   12.56 -     | SOME name => value_select name;
   12.57 -  
   12.58 -fun value_cmd some_name modes raw_t state =
   12.59 +fun value_cmd modes raw_t state =
   12.60    let
   12.61      val ctxt = Toplevel.context_of state;
   12.62      val t = Syntax.read_term ctxt raw_t;
   12.63 -    val t' = value_maybe_select some_name ctxt t;
   12.64 +    val t' = value ctxt t;
   12.65      val ty' = Term.type_of t';
   12.66      val ctxt' = Variable.auto_fixes t' ctxt;
   12.67      val p = Print_Mode.with_modes modes (fn () =>
   12.68 @@ -63,14 +40,14 @@
   12.69    
   12.70  val _ =
   12.71    Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
   12.72 -    (opt_evaluator -- opt_modes -- Parse.term
   12.73 -      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
   12.74 +    (opt_modes -- Parse.term
   12.75 +      >> (fn (modes, t) => Toplevel.keep (value_cmd modes t)));
   12.76  
   12.77  val _ = Context.>> (Context.map_theory
   12.78    (Thy_Output.antiquotation @{binding value}
   12.79 -    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
   12.80 -    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
   12.81 +    (Term_Style.parse -- Args.term)
   12.82 +    (fn {source, context, ...} => fn (style, t) => Thy_Output.output context
   12.83        (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
   12.84 -        [style (value_maybe_select some_name context t)]))));
   12.85 +        [style (value context t)]))));
   12.86  
   12.87  end;
    13.1 --- a/src/HOL/ex/Eval_Examples.thy	Fri May 09 08:13:36 2014 +0200
    13.2 +++ b/src/HOL/ex/Eval_Examples.thy	Fri May 09 08:13:37 2014 +0200
    13.3 @@ -25,36 +25,20 @@
    13.4  text {* term evaluation *}
    13.5  
    13.6  value "(Suc 2 + 1) * 4"
    13.7 -value [code] "(Suc 2 + 1) * 4"
    13.8 -value [nbe] "(Suc 2 + 1) * 4"
    13.9  
   13.10  value "(Suc 2 + Suc 0) * Suc 3"
   13.11 -value [code] "(Suc 2 + Suc 0) * Suc 3"
   13.12 -value [nbe] "(Suc 2 + Suc 0) * Suc 3"
   13.13  
   13.14  value "nat 100"
   13.15 -value [code] "nat 100"
   13.16 -value [nbe] "nat 100"
   13.17  
   13.18  value "(10::int) \<le> 12"
   13.19 -value [code] "(10::int) \<le> 12"
   13.20 -value [nbe] "(10::int) \<le> 12"
   13.21  
   13.22  value "max (2::int) 4"
   13.23 -value [code] "max (2::int) 4"
   13.24 -value [nbe] "max (2::int) 4"
   13.25  
   13.26  value "of_int 2 / of_int 4 * (1::rat)"
   13.27 -value [code] "of_int 2 / of_int 4 * (1::rat)"
   13.28 -value [nbe] "of_int 2 / of_int 4 * (1::rat)"
   13.29  
   13.30  value "[] :: nat list"
   13.31 -value [code] "[] :: nat list"
   13.32 -value [nbe] "[] :: nat list"
   13.33  
   13.34  value "[(nat 100, ())]"
   13.35 -value [code] "[(nat 100, ())]"
   13.36 -value [nbe] "[(nat 100, ())]"
   13.37  
   13.38  text {* a fancy datatype *}
   13.39  
   13.40 @@ -67,7 +51,5 @@
   13.41    | Blubb "('a, 'b) foo"
   13.42  
   13.43  value "Bla (Bar (4::nat) [Suc 0])"
   13.44 -value [code] "Bla (Bar (4::nat) [Suc 0])"
   13.45 -value [nbe] "Bla (Bar (4::nat) [Suc 0])"
   13.46  
   13.47  end
    14.1 --- a/src/HOL/ex/Normalization_by_Evaluation.thy	Fri May 09 08:13:36 2014 +0200
    14.2 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Fri May 09 08:13:37 2014 +0200
    14.3 @@ -68,20 +68,20 @@
    14.4  lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
    14.5    by normalization rule
    14.6  lemma "rev [a, b, c] = [c, b, a]" by normalization
    14.7 -value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
    14.8 -value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
    14.9 -value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
   14.10 -value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
   14.11 +value "rev (a#b#cs) = rev cs @ [b, a]"
   14.12 +value "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
   14.13 +value "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
   14.14 +value "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
   14.15  lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" 
   14.16    by normalization
   14.17 -value [nbe] "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
   14.18 -value [nbe] "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
   14.19 +value "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
   14.20 +value "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
   14.21  lemma "let x = y in [x, x] = [y, y]" by normalization
   14.22  lemma "Let y (%x. [x,x]) = [y, y]" by normalization
   14.23 -value [nbe] "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
   14.24 +value "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
   14.25  lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
   14.26 -value [nbe] "filter (%x. x) ([True,False,x]@xs)"
   14.27 -value [nbe] "filter Not ([True,False,x]@xs)"
   14.28 +value "filter (%x. x) ([True,False,x]@xs)"
   14.29 +value "filter Not ([True,False,x]@xs)"
   14.30  
   14.31  lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
   14.32  lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
   14.33 @@ -106,7 +106,7 @@
   14.34  lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
   14.35  lemma "max (Suc 0) 0 = Suc 0" by normalization
   14.36  lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
   14.37 -value [nbe] "Suc 0 \<in> set ms"
   14.38 +value "Suc 0 \<in> set ms"
   14.39  
   14.40  (* non-left-linear patterns, equality by extensionality *)
   14.41  
   14.42 @@ -115,13 +115,13 @@
   14.43  lemma "(f o g) x = f (g x)" by normalization
   14.44  lemma "(f o id) x = f x" by normalization
   14.45  lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
   14.46 -value [nbe] "(\<lambda>x. x)"
   14.47 +value "(\<lambda>x. x)"
   14.48  
   14.49  (* Church numerals: *)
   14.50  
   14.51 -value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
   14.52 -value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
   14.53 -value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
   14.54 +value "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
   14.55 +value "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
   14.56 +value "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
   14.57  
   14.58  (* handling of type classes in connection with equality *)
   14.59  
    15.1 --- a/src/HOL/ex/Parallel_Example.thy	Fri May 09 08:13:36 2014 +0200
    15.2 +++ b/src/HOL/ex/Parallel_Example.thy	Fri May 09 08:13:37 2014 +0200
    15.3 @@ -93,7 +93,7 @@
    15.4     (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic
    15.5       in (computation_primes (), Parallel.join c))"
    15.6  
    15.7 -value [code] "computation_future ()"
    15.8 +value "computation_future ()"
    15.9  
   15.10  definition computation_factorise :: "nat \<Rightarrow> nat list" where
   15.11    "computation_factorise = Debug.timing (STR ''factorise'') factorise"
   15.12 @@ -102,7 +102,7 @@
   15.13    "computation_parallel _ = Debug.timing (STR ''overall computation'')
   15.14       (Parallel.map computation_factorise) [20000..<20100]"
   15.15  
   15.16 -value [code] "computation_parallel ()"
   15.17 +value "computation_parallel ()"
   15.18  
   15.19  end
   15.20