# HG changeset patch
# User wenzelm
# Date 891682946 -7200
# Node ID b54c337f2c7feb5f2c43f97b54bdf7c71ff7a594
# Parent  90fc96d16df44c3811a010a5e4c09acb8c00e5ee
added Goal_def;

diff -r 90fc96d16df4 -r b54c337f2c7f src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Apr 04 11:41:24 1998 +0200
+++ b/src/Pure/pure_thy.ML	Sat Apr 04 11:42:26 1998 +0200
@@ -257,8 +257,7 @@
 
 val proto_pure =
   Theory.pre_pure
-  |> Attribute.setup
-  |> theorems_setup
+  |> Theory.setup [Attribute.setup, theorems_setup]
   |> Theory.add_types
    (("fun", 2, NoSyn) ::
     ("prop", 0, NoSyn) ::
@@ -281,9 +280,12 @@
     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
+    ("Goal", "prop => prop", Mixfix ("GOAL _", [999], 1000)),
     ("TYPE", "'a itself", NoSyn)]
   |> Theory.add_path "ProtoPure"
-  |> add_store_defs [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]
+  |> add_store_defs
+   [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),
+    ("Goal_def", "GOAL (PROP A) == PROP A")]
   |> Theory.add_name "ProtoPure";
 
 val pure =
@@ -313,6 +315,7 @@
 struct
   val thy = PureThy.proto_pure;
   val flexpair_def = get_axiom thy "flexpair_def";
+  val Goal_def = get_axiom thy "Goal_def";
 end;
 
 structure Pure = struct val thy = PureThy.pure end;