From ff5454812f9e2720bd90c3a5437505644f63b487 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 31 Jul 2020 14:56:24 +0200
Subject: (FEAT) Term elaboration of assumption and goal statements.   .
 spartan/core/goals.ML   . spartan/core/elaboration.ML   .
 spartan/core/elaborated_statement.ML

(FEAT) More context tacticals and search tacticals.
  . spartan/core/context_tactical.ML

(FEAT) Improved subgoal focus.
  Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
  . spartan/core/focus.ML

(FIX) Normalize facts in order to be able to resolve properly.
  . spartan/core/typechecking.ML

(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.
---
 spartan/core/goals.ML | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'spartan/core/goals.ML')

diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index 87ec2b8..540f5c7 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -1,9 +1,9 @@
 (*  Title:      goals.ML
-    Author:     Makarius Wenzel, Joshua Chen
+    Author:     Joshua Chen
 
 Goal statements and proof term export.
 
-Modified from code originally written by Makarius Wenzel.
+Modified from code contained in ~~/Pure/Isar/specification.ML.
 *)
 
 local
@@ -184,15 +184,15 @@ val schematic_theorem_cmd =
   gen_schematic_theorem
     Bundle.includes_cmd
     Attrib.check_src
-    Elaborated_Assumption.read_goal_statement
+    Elaborated_Statement.read_goal_statement
 
 fun theorem spec descr =
   Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) 
-    ( Scan.option (Args.parens (Args.$$$ "derive"))
+    ( Scan.option (Args.parens (Args.$$$ "def"))
       -- (long_statement || short_statement) >>
         (fn (opt_derive, (long, binding, includes, elems, concl)) =>
           schematic_theorem_cmd
-            (case opt_derive of SOME "derive" => true | _ => false)
+            (case opt_derive of SOME "def" => true | _ => false)
             long descr NONE (K I) binding includes elems concl) )
 
 fun definition spec descr =
-- 
cgit v1.2.3