eliminated GOAL syntax;
authorwenzelm
Wed Dec 13 17:43:33 2000 +0100 (2000-12-13)
changeset 1066775a1c9575edb
parent 10666 d2a7c5be62be
child 10668 3b84288e60b7
eliminated GOAL syntax;
src/Pure/drule.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/drule.ML	Wed Dec 13 17:41:10 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Dec 13 17:43:33 2000 +0100
     1.3 @@ -703,17 +703,18 @@
     1.4      flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
     1.5  
     1.6  
     1.7 -(*** GOAL (PROP A) <==> PROP A ***)
     1.8 +(*** Goal (PROP A) <==> PROP A ***)
     1.9  
    1.10  local
    1.11 -  val A = read_prop "PROP A";
    1.12 -  val G = read_prop "GOAL (PROP A)";
    1.13 +  val cert = Thm.cterm_of proto_sign;
    1.14 +  val A = Free ("A", propT);
    1.15 +  val G = Logic.mk_goal A;
    1.16    val (G_def, _) = freeze_thaw ProtoPure.Goal_def;
    1.17  in
    1.18 -  val triv_goal = store_thm "triv_goal"
    1.19 -    (tag_rule internal_tag (standard (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume A))));
    1.20 -  val rev_triv_goal = store_thm "rev_triv_goal"
    1.21 -    (tag_rule internal_tag (standard (Thm.equal_elim G_def (Thm.assume G))));
    1.22 +  val triv_goal = store_thm "triv_goal" (tag_rule internal_tag (standard
    1.23 +      (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume (cert A)))));
    1.24 +  val rev_triv_goal = store_thm "rev_triv_goal" (tag_rule internal_tag (standard
    1.25 +      (Thm.equal_elim G_def (Thm.assume (cert G)))));
    1.26  end;
    1.27  
    1.28  val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const);
     2.1 --- a/src/Pure/pure_thy.ML	Wed Dec 13 17:41:10 2000 +0100
     2.2 +++ b/src/Pure/pure_thy.ML	Wed Dec 13 17:43:33 2000 +0100
     2.3 @@ -137,7 +137,7 @@
     2.4      val ref {space, thms_tab, ...} = get_theorems thy;
     2.5    in
     2.6      fn name =>
     2.7 -      apsome (map (Thm.transfer_sg (Sign.deref sg_ref)))  	(*semi-dynamic identity*)
     2.8 +      apsome (map (Thm.transfer_sg (Sign.deref sg_ref)))        (*semi-dynamic identity*)
     2.9        (Symtab.lookup (thms_tab, NameSpace.intern space name))   (*static content*)
    2.10    end;
    2.11  
    2.12 @@ -474,7 +474,7 @@
    2.13      ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
    2.14      ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    2.15      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
    2.16 -    ("Goal", "prop => prop", Mixfix ("GOAL _", [1000], 999)),
    2.17 +    ("Goal", "prop => prop", NoSyn),
    2.18      ("TYPE", "'a itself", NoSyn),
    2.19      (Term.dummy_patternN, "'a", Delimfix "'_")]
    2.20    |> Theory.add_modesyntax ("", false)
    2.21 @@ -482,8 +482,9 @@
    2.22        :: Syntax.pure_appl_syntax)
    2.23    |> local_path
    2.24    |> (#1 oo (add_defs false o map Thm.no_attributes))
    2.25 -   [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),
    2.26 -    ("Goal_def", "GOAL (PROP A) == PROP A")]
    2.27 +   [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]
    2.28 +  |> (#1 oo (add_defs_i false o map Thm.no_attributes))
    2.29 +   [("Goal_def", let val A = Free ("A", propT) in Logic.mk_equals (Logic.mk_goal A, A) end)]
    2.30    |> (#1 o add_thmss [(("nothing", []), [])])
    2.31    |> end_theory;
    2.32