src/Tools/isac/ProgLang/ListC.thy
changeset 59484 c5f3da9e3645
parent 59472 3e904f8ec16c
child 59577 60d191402598
     1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Wed Dec 12 19:52:53 2018 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Fri Dec 14 18:46:04 2018 +0100
     1.3 @@ -130,10 +130,8 @@
     1.4  remdups_Nil:	"remdups [] = []" and
     1.5  remdups_Cons:	"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 
     1.6  
     1.7 -(** Lexicographic orderings on lists ...!!!**)
     1.8 -
     1.9 -ML\<open>(*the former ListC.ML*)
    1.10 -(** rule set for evaluating listexpr in scripts **)
    1.11 +ML\<open>
    1.12 +(** rule set for evaluating listexpr in scripts, will be extended in several thys **)
    1.13  val list_rls = 
    1.14    Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 
    1.15      erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],