src/Provers/simplifier.ML
changeset 5928 6e00a206a948
parent 5886 0373323180f5
child 6096 3451f9e88528
     1.1 --- a/src/Provers/simplifier.ML	Wed Nov 18 11:02:20 1998 +0100
     1.2 +++ b/src/Provers/simplifier.ML	Wed Nov 18 11:02:42 1998 +0100
     1.3 @@ -89,6 +89,7 @@
     1.4    val simp_del_global: theory attribute
     1.5    val simp_add_local: Proof.context attribute
     1.6    val simp_del_local: Proof.context attribute
     1.7 +  val simp_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -402,13 +403,14 @@
    1.12  
    1.13  (* add / del *)
    1.14  
    1.15 -val simp_addN = "add";
    1.16 -val simp_delN = "del";
    1.17 -val simp_ignoreN = "other";
    1.18 +val simpN = "simp";
    1.19 +val addN = "add";
    1.20 +val delN = "del";
    1.21 +val otherN = "other";
    1.22  
    1.23  fun simp_att change =
    1.24 -  (Args.$$$ simp_addN >> K (op addsimps) ||
    1.25 -    Args.$$$ simp_delN >> K (op delsimps) ||
    1.26 +  (Args.$$$ addN >> K (op addsimps) ||
    1.27 +    Args.$$$ delN >> K (op delsimps) ||
    1.28      Scan.succeed (op addsimps))
    1.29    >> change
    1.30    |> Scan.lift
    1.31 @@ -427,7 +429,7 @@
    1.32  (* setup_attrs *)
    1.33  
    1.34  val setup_attrs = Attrib.add_attributes
    1.35 - [("simp",              simp_attr, "simplification rule"),
    1.36 + [(simpN,               simp_attr, "simplification rule"),
    1.37    ("simplify",          conv_attr simplify, "simplify rule"),
    1.38    ("asm_simplify",      conv_attr asm_simplify, "simplify rule, using assumptions"),
    1.39    ("full_simplify",     conv_attr full_simplify, "fully simplify rule"),
    1.40 @@ -439,11 +441,17 @@
    1.41  
    1.42  (* simplification *)
    1.43  
    1.44 -val simp_args =
    1.45 -  Method.only_sectioned_args
    1.46 -   [Args.$$$ simp_addN >> K simp_add_local,
    1.47 -    Args.$$$ simp_delN >> K simp_del_local,
    1.48 -    Args.$$$ simp_ignoreN >> K I];
    1.49 +val simp_modifiers =
    1.50 + [Args.$$$ simpN -- Args.$$$ addN >> K simp_add_local,
    1.51 +  Args.$$$ simpN -- Args.$$$ delN >> K simp_del_local,
    1.52 +  Args.$$$ otherN >> K I];	(* FIXME ?? *)
    1.53 +
    1.54 +val simp_modifiers' =
    1.55 + [Args.$$$ addN >> K simp_add_local,
    1.56 +  Args.$$$ delN >> K simp_del_local,
    1.57 +  Args.$$$ otherN >> K I];
    1.58 +
    1.59 +val simp_args = Method.only_sectioned_args simp_modifiers';
    1.60  
    1.61  fun simp_meth tac ctxt = Method.METHOD (fn facts =>
    1.62    FIRSTGOAL (REPEAT_DETERM o etac Drule.thin_rl THEN'
    1.63 @@ -456,7 +464,7 @@
    1.64  (* setup_methods *)
    1.65  
    1.66  val setup_methods = Method.add_methods
    1.67 - [("simp",              simp_method asm_full_simp_tac, "simplification"),
    1.68 + [(simpN,               simp_method asm_full_simp_tac, "simplification"),
    1.69    ("simp_tac",          simp_method simp_tac, "simp_tac"),
    1.70    ("asm_simp_tac",      simp_method asm_simp_tac, "asm_simp_tac"),
    1.71    ("full_simp_tac",     simp_method full_simp_tac, "full_simp_tac"),